Let x be given.
Assume Hx: x ∈ R_omega_space.
Apply set_ext to the current goal.
An exact proof term for the current goal is (Romega_D_scaled_diffs_diag_subset0 x Hx).
Let a be given.
Assume Ha0: a ∈ {0}.
We will prove a ∈ Romega_D_scaled_diffs x x.
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).
We will prove 0 ∈ Romega_D_scaled_diffs x x.
We prove the intermediate claim H0omega: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim HxiR: apply_fun x 0 ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R x 0 Hx H0omega).
We prove the intermediate claim Hbd0: R_bounded_distance (apply_fun x 0) (apply_fun x 0) = 0.
An exact proof term for the current goal is (R_bounded_distance_self_zero (apply_fun x 0) HxiR).
We prove the intermediate claim H10: ordsucc 0 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc 0 H0omega).
We prove the intermediate claim HinvR: inv_nat (ordsucc 0) ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc 0) H10).
We prove the intermediate claim HinvS: SNo (inv_nat (ordsucc 0)).
An exact proof term for the current goal is (real_SNo (inv_nat (ordsucc 0)) HinvR).
We prove the intermediate claim Hdef: 0 = mul_SNo (R_bounded_distance (apply_fun x 0) (apply_fun x 0)) (inv_nat (ordsucc 0)).
rewrite the current goal using Hbd0 (from left to right).
rewrite the current goal using (mul_SNo_zeroL (inv_nat (ordsucc 0)) HinvS) (from left to right).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (ReplI ω (λi : set ⇒ mul_SNo (R_bounded_distance (apply_fun x i) (apply_fun x i)) (inv_nat (ordsucc i))) 0 H0omega).
∎