Let x and y be given.
Assume Hx: x ∈ R_omega_space.
Assume Hy: y ∈ R_omega_space.
Apply (ReplEq_ext ω (λi : set ⇒ mul_SNo (R_bounded_distance (apply_fun x i) (apply_fun y i)) (inv_nat (ordsucc i))) (λi : set ⇒ mul_SNo (R_bounded_distance (apply_fun y i) (apply_fun x i)) (inv_nat (ordsucc i)))) to the current goal.
Let i be given.
Assume HiO: i ∈ ω.
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 Hbd: R_bounded_distance (apply_fun x i) (apply_fun y i) = R_bounded_distance (apply_fun y i) (apply_fun x i).
An exact proof term for the current goal is (R_bounded_distance_sym (apply_fun x i) (apply_fun y i) HxiR HyiR).
rewrite the current goal using Hbd (from left to right).
Use reflexivity.
∎