Let f and g be given.
Assume Hf: f ∈ real_sequences.
Assume Hg: g ∈ real_sequences.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is real_1.
Let a be given.
Assume HaA: a ∈ Romega_clipped_diffs f g.
Assume HaR: a ∈ R.
We will prove Rle a 1.
Apply (RleI a 1 HaR real_1) to the current goal.
Assume Hlt1: Rlt 1 a.
We will prove False.
Apply (ReplE_impred ω (λn : set ⇒ Romega_coord_clipped_diff f g n) a HaA False) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
Assume Han: a = Romega_coord_clipped_diff f g n.
We prove the intermediate claim Hlt': Rlt 1 (Romega_coord_clipped_diff f g n).
rewrite the current goal using Han (from right to left).
An exact proof term for the current goal is Hlt1.
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).
Set t to be the term add_SNo (apply_fun f n) (minus_SNo (apply_fun g n)).
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 HabsR: abs_SNo t ∈ R.
Apply (xm (0 ≤ t) (abs_SNo t ∈ R)) to the current goal.
Assume H0le: 0 ≤ t.
We prove the intermediate claim Habseq: abs_SNo t = t.
An exact proof term for the current goal is (nonneg_abs_SNo t H0le).
rewrite the current goal using Habseq (from left to right).
An exact proof term for the current goal is HtR.
Assume Hn0le: ¬ (0 ≤ t).
We prove the intermediate claim HmtR: minus_SNo t ∈ R.
An exact proof term for the current goal is (real_minus_SNo t HtR).
We prove the intermediate claim Habseq: abs_SNo t = minus_SNo t.
An exact proof term for the current goal is (not_nonneg_abs_SNo t Hn0le).
rewrite the current goal using Habseq (from left to right).
An exact proof term for the current goal is HmtR.
We prove the intermediate claim HabsDef: Romega_coord_abs_diff f g n = abs_SNo t.
Use reflexivity.
We prove the intermediate claim HabsDiffR: Romega_coord_abs_diff f g n ∈ R.
rewrite the current goal using HabsDef (from left to right).
An exact proof term for the current goal is HabsR.
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.
Apply (xm (Rlt (Romega_coord_abs_diff f g n) 1) False) to the current goal.
Assume Hlt: Rlt (Romega_coord_abs_diff f g n) 1.
We prove the intermediate claim Hnlt1abs: ¬ (Rlt 1 (Romega_coord_abs_diff f g n)).
An exact proof term for the current goal is (not_Rlt_sym (Romega_coord_abs_diff f g n) 1 Hlt).
We prove the intermediate claim HclEq: Romega_coord_clipped_diff f g n = Romega_coord_abs_diff f g n.
rewrite the current goal using Hdef (from left to right).
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).
Use reflexivity.
We prove the intermediate claim Hlt1abs: Rlt 1 (Romega_coord_abs_diff f g n).
rewrite the current goal using HclEq (from right to left).
An exact proof term for the current goal is Hlt'.
An exact proof term for the current goal is (Hnlt1abs Hlt1abs).
Assume Hnlt: ¬ (Rlt (Romega_coord_abs_diff f g n) 1).
We prove the intermediate claim HclEq: Romega_coord_clipped_diff f g n = 1.
rewrite the current goal using Hdef (from left to right).
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).
Use reflexivity.
We prove the intermediate claim Hlt11: Rlt 1 1.
rewrite the current goal using HclEq (from right to left) at position 2.
An exact proof term for the current goal is Hlt'.
An exact proof term for the current goal is (not_Rlt_refl 1 real_1 Hlt11).
∎