Let f and g be given.
Assume Hf: f ∈ real_sequences.
Assume Hg: g ∈ real_sequences.
Apply (ReplEq_ext ω (λn : set ⇒ Romega_coord_clipped_diff f g n) (λn : set ⇒ Romega_coord_clipped_diff g f n)) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
We prove the intermediate claim Hfpack: total_function_on f ω R ∧ functional_graph f.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod ω R)) (λf0 : set ⇒ total_function_on f0 ω R ∧ functional_graph f0) f Hf).
We prove the intermediate claim Hgpack: total_function_on g ω R ∧ functional_graph g.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod ω R)) (λg0 : set ⇒ total_function_on g0 ω R ∧ functional_graph g0) g Hg).
We prove the intermediate claim Htotf: total_function_on f ω R.
An exact proof term for the current goal is (andEL (total_function_on f ω R) (functional_graph f) Hfpack).
We prove the intermediate claim Htotg: total_function_on g ω R.
An exact proof term for the current goal is (andEL (total_function_on g ω R) (functional_graph g) Hgpack).
We prove the intermediate claim HfnR: apply_fun f n ∈ R.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y f ω R n Htotf HnO).
We prove the intermediate claim HgnR: apply_fun g n ∈ R.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y g ω R n Htotg HnO).
We prove the intermediate claim HfnS: SNo (apply_fun f n).
An exact proof term for the current goal is (real_SNo (apply_fun f n) HfnR).
We prove the intermediate claim HgnS: SNo (apply_fun g n).
An exact proof term for the current goal is (real_SNo (apply_fun g n) HgnR).
We prove the intermediate claim Habs: Romega_coord_abs_diff f g n = Romega_coord_abs_diff g f n.
An exact proof term for the current goal is (abs_SNo_dist_swap (apply_fun f n) (apply_fun g n) HfnS HgnS).
We prove the intermediate claim Hdef1: Romega_coord_clipped_diff f g n = If_i (Rlt (Romega_coord_abs_diff f g n) 1) (Romega_coord_abs_diff f g n) 1.
Use reflexivity.
We prove the intermediate claim Hdef2: Romega_coord_clipped_diff g f n = If_i (Rlt (Romega_coord_abs_diff g f n) 1) (Romega_coord_abs_diff g f n) 1.
Use reflexivity.
rewrite the current goal using Hdef1 (from left to right).
rewrite the current goal using Hdef2 (from left to right).
rewrite the current goal using Habs (from left to right).
Use reflexivity.
∎