Let f, g and n be given.
Assume Hf: f ∈ real_sequences.
Assume Hg: g ∈ real_sequences.
Assume HnO: n ∈ ω.
Set t to be the term add_SNo (apply_fun f n) (minus_SNo (apply_fun g 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 HmgnR: minus_SNo (apply_fun g n) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (apply_fun g n) HgnR).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun f n) HfnR (minus_SNo (apply_fun g n)) HmgnR).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HabsNN: 0 ≤ abs_SNo t.
An exact proof term for the current goal is (abs_SNo_nonneg t HtS).
We prove the intermediate claim HdefAbs: Romega_coord_abs_diff f g n = abs_SNo t.
Use reflexivity.
We prove the intermediate claim Hdef: 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.
rewrite the current goal using Hdef (from left to right).
Apply (xm (Rlt (Romega_coord_abs_diff f g n) 1) (0 ≤ If_i (Rlt (Romega_coord_abs_diff f g n) 1) (Romega_coord_abs_diff f g n) 1)) to the current goal.
Assume Hlt: Rlt (Romega_coord_abs_diff f g n) 1.
rewrite the current goal using (If_i_1 (Rlt (Romega_coord_abs_diff f g n) 1) (Romega_coord_abs_diff f g n) 1 Hlt) (from left to right).
rewrite the current goal using HdefAbs (from left to right).
An exact proof term for the current goal is HabsNN.
Assume Hnlt: ¬ (Rlt (Romega_coord_abs_diff f g n) 1).
rewrite the current goal using (If_i_0 (Rlt (Romega_coord_abs_diff f g n) 1) (Romega_coord_abs_diff f g n) 1 Hnlt) (from left to right).
An exact proof term for the current goal is (SNoLtLe 0 1 SNoLt_0_1).
∎