Let x be given.
Assume Hx: x ∈ R_omega_space.
Let a be given.
Assume Ha: a ∈ Romega_D_scaled_diffs x x.
We will prove a ∈ {0}.
Apply (ReplE_impred ω (λi : set ⇒ mul_SNo (R_bounded_distance (apply_fun x i) (apply_fun x i)) (inv_nat (ordsucc i))) a Ha (a ∈ {0})) to the current goal.
Let i be given.
Assume HiO: i ∈ ω.
Assume Hai: a = mul_SNo (R_bounded_distance (apply_fun x i) (apply_fun x i)) (inv_nat (ordsucc i)).
rewrite the current goal using Hai (from left to right).
We prove the intermediate claim HxiR: apply_fun x i ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R x i Hx HiO).
We prove the intermediate claim Hbd0: R_bounded_distance (apply_fun x i) (apply_fun x i) = 0.
An exact proof term for the current goal is (R_bounded_distance_self_zero (apply_fun x i) HxiR).
rewrite the current goal using Hbd0 (from left to right).
We prove the intermediate claim HSi: ordsucc i ∈ ω.
An exact proof term for the current goal is (omega_ordsucc i HiO).
We prove the intermediate claim HinvR: inv_nat (ordsucc i) ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc i) HSi).
We prove the intermediate claim HinvS: SNo (inv_nat (ordsucc i)).
An exact proof term for the current goal is (real_SNo (inv_nat (ordsucc i)) HinvR).
rewrite the current goal using (mul_SNo_zeroL (inv_nat (ordsucc i)) HinvS) (from left to right).
An exact proof term for the current goal is (SingI 0).
∎