Let f, g, h and n be given.
Assume Hf: f ∈ real_sequences.
Assume Hg: g ∈ real_sequences.
Assume Hh: h ∈ real_sequences.
Assume HnO: n ∈ ω.
Set r to be the term Romega_coord_abs_diff f h n.
Set p to be the term Romega_coord_abs_diff f g n.
Set q to be the term Romega_coord_abs_diff g h n.
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (Romega_coord_abs_diff_in_R f h n Hf Hh HnO).
We prove the intermediate claim HpR: p ∈ R.
An exact proof term for the current goal is (Romega_coord_abs_diff_in_R f g n Hf Hg HnO).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (Romega_coord_abs_diff_in_R g h n Hg Hh HnO).
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
We prove the intermediate claim HpS: SNo p.
An exact proof term for the current goal is (real_SNo p HpR).
We prove the intermediate claim HqS: SNo q.
An exact proof term for the current goal is (real_SNo q HqR).
We prove the intermediate claim HabsTri: r ≤ add_SNo p q.
An exact proof term for the current goal is (Romega_coord_abs_diff_triangle f g h n Hf Hg Hh HnO).
We prove the intermediate claim HppNN: 0 ≤ p.
Set t to be the term add_SNo (apply_fun f n) (minus_SNo (apply_fun g n)).
We prove the intermediate claim HtS: SNo t.
We prove the intermediate claim HtR: t ∈ R.
We prove the intermediate claim Ht1R: apply_fun f n ∈ R.
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 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).
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 Ht2R: minus_SNo (apply_fun g n) ∈ R.
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 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 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).
An exact proof term for the current goal is (real_minus_SNo (apply_fun g n) HgnR).
An exact proof term for the current goal is (real_add_SNo (apply_fun f n) Ht1R (minus_SNo (apply_fun g n)) Ht2R).
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim Hdef: p = abs_SNo t.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (abs_SNo_nonneg t HtS).
We prove the intermediate claim HqqNN: 0 ≤ q.
Set t to be the term add_SNo (apply_fun g n) (minus_SNo (apply_fun h n)).
We prove the intermediate claim HtS: SNo t.
We prove the intermediate claim HtR: t ∈ R.
We prove the intermediate claim Ht1R: apply_fun g n ∈ R.
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 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).
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 Ht2R: minus_SNo (apply_fun h n) ∈ R.
We prove the intermediate claim Hhpack: total_function_on h ω R ∧ functional_graph h.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod ω R)) (λh0 : set ⇒ total_function_on h0 ω R ∧ functional_graph h0) h Hh).
We prove the intermediate claim Htoth: total_function_on h ω R.
An exact proof term for the current goal is (andEL (total_function_on h ω R) (functional_graph h) Hhpack).
We prove the intermediate claim HhnR: apply_fun h n ∈ R.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y h ω R n Htoth HnO).
An exact proof term for the current goal is (real_minus_SNo (apply_fun h n) HhnR).
An exact proof term for the current goal is (real_add_SNo (apply_fun g n) Ht1R (minus_SNo (apply_fun h n)) Ht2R).
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim Hdef: q = abs_SNo t.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (abs_SNo_nonneg t HtS).
We prove the intermediate claim HdefL: Romega_coord_clipped_diff f h n = If_i (Rlt r 1) r 1.
Use reflexivity.
We prove the intermediate claim HdefR1: Romega_coord_clipped_diff f g n = If_i (Rlt p 1) p 1.
Use reflexivity.
We prove the intermediate claim HdefR2: Romega_coord_clipped_diff g h n = If_i (Rlt q 1) q 1.
Use reflexivity.
rewrite the current goal using HdefL (from left to right).
rewrite the current goal using HdefR1 (from left to right).
rewrite the current goal using HdefR2 (from left to right).
We prove the intermediate claim Hmono: If_i (Rlt r 1) r 1 ≤ If_i (Rlt (add_SNo p q) 1) (add_SNo p q) 1.
An exact proof term for the current goal is (Rclip_mono r (add_SNo p q) HrR (real_add_SNo p HpR q HqR) HabsTri).
We prove the intermediate claim Hsub: If_i (Rlt (add_SNo p q) 1) (add_SNo p q) 1 ≤ add_SNo (If_i (Rlt p 1) p 1) (If_i (Rlt q 1) q 1).
An exact proof term for the current goal is (Rclip_subadd_nonneg p q HpR HqR HppNN HqqNN).
An exact proof term for the current goal is (SNoLe_tra (If_i (Rlt r 1) r 1) (If_i (Rlt (add_SNo p q) 1) (add_SNo p q) 1) (add_SNo (If_i (Rlt p 1) p 1) (If_i (Rlt q 1) q 1)) (SNo_If_i (Rlt r 1) r 1 HrS SNo_1) (SNo_If_i (Rlt (add_SNo p q) 1) (add_SNo p q) 1 (SNo_add_SNo p q HpS HqS) SNo_1) (SNo_add_SNo (If_i (Rlt p 1) p 1) (If_i (Rlt q 1) q 1) (SNo_If_i (Rlt p 1) p 1 HpS SNo_1) (SNo_If_i (Rlt q 1) q 1 HqS SNo_1)) Hmono Hsub).
∎