Let J and f be given.
Assume HJne: J ≠ Empty.
Assume Hf: f ∈ power_real J.
Set A to be the term power_real_clipped_diffs J f f.
Apply set_ext to the current goal.
Let a be given.
Assume HaA: a ∈ A.
We will prove a ∈ {0}.
Apply (ReplE_impred J (λj : set ⇒ power_real_coord_clipped_diff f f j) a HaA (a ∈ {0})) to the current goal.
Let j be given.
Assume HjJ: j ∈ J.
Assume Haj: a = power_real_coord_clipped_diff f f j.
rewrite the current goal using Haj (from left to right).
We prove the intermediate claim HfjR: apply_fun f j ∈ R.
An exact proof term for the current goal is (power_real_coord_in_R J f j HjJ Hf).
rewrite the current goal using (power_real_coord_clipped_diff_eq_R_bounded_distance J f f j HjJ Hf Hf) (from left to right).
rewrite the current goal using (R_bounded_distance_self_zero (apply_fun f j) HfjR) (from left to right).
An exact proof term for the current goal is (SingI 0).
Let a be given.
Assume Ha0: a ∈ {0}.
We will prove a ∈ A.
We prove the intermediate claim Haeq: a = 0.
An exact proof term for the current goal is (SingE 0 a Ha0).
rewrite the current goal using Haeq (from left to right).
Apply (nonempty_has_element J HJne) to the current goal.
Let j0 be given.
Assume Hj0: j0 ∈ J.
We prove the intermediate claim H0eq: power_real_coord_clipped_diff f f j0 = 0.
We prove the intermediate claim Hj0R: apply_fun f j0 ∈ R.
An exact proof term for the current goal is (power_real_coord_in_R J f j0 Hj0 Hf).
rewrite the current goal using (power_real_coord_clipped_diff_eq_R_bounded_distance J f f j0 Hj0 Hf Hf) (from left to right).
An exact proof term for the current goal is (R_bounded_distance_self_zero (apply_fun f j0) Hj0R).
rewrite the current goal using H0eq (from right to left).
An exact proof term for the current goal is (ReplI J (λj : set ⇒ power_real_coord_clipped_diff f f j) j0 Hj0).
∎