Let x and y be given.
Assume Hx: x ∈ R_omega_space.
Assume Hy: y ∈ R_omega_space.
Let a be given.
Assume Ha: a ∈ Romega_D_scaled_diffs x y.
We will prove a ∈ R.
Apply (ReplE ω (λi : set ⇒ mul_SNo (R_bounded_distance (apply_fun x i) (apply_fun y i)) (inv_nat (ordsucc i))) a Ha) to the current goal.
Let i be given.
Assume Hiconj.
We prove the intermediate claim HiO: i ∈ ω.
An exact proof term for the current goal is (andEL (i ∈ ω) (a = mul_SNo (R_bounded_distance (apply_fun x i) (apply_fun y i)) (inv_nat (ordsucc i))) Hiconj).
We prove the intermediate claim Hai: a = mul_SNo (R_bounded_distance (apply_fun x i) (apply_fun y i)) (inv_nat (ordsucc i)).
An exact proof term for the current goal is (andER (i ∈ ω) (a = mul_SNo (R_bounded_distance (apply_fun x i) (apply_fun y i)) (inv_nat (ordsucc i))) Hiconj).
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 HyiR: apply_fun y i ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R y i Hy HiO).
We prove the intermediate claim HbdR: R_bounded_distance (apply_fun x i) (apply_fun y i) ∈ R.
An exact proof term for the current goal is (R_bounded_distance_in_R (apply_fun x i) (apply_fun y i) HxiR HyiR).
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 HmulR: mul_SNo (R_bounded_distance (apply_fun x i) (apply_fun y i)) (inv_nat (ordsucc i)) ∈ R.
An exact proof term for the current goal is (real_mul_SNo (R_bounded_distance (apply_fun x i) (apply_fun y i)) HbdR (inv_nat (ordsucc i)) HinvR).
rewrite the current goal using Hai (from left to right).
An exact proof term for the current goal is HmulR.
∎