Let f and g be given.
Assume Hf: f ∈ real_sequences.
Assume Hg: g ∈ real_sequences.
Let a be given.
Assume HaA: a ∈ Romega_clipped_diffs f g.
We will prove a ∈ R.
Apply (ReplE_impred ω (λn : set ⇒ Romega_coord_clipped_diff f g n) a HaA (a ∈ R)) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
Assume Han: a = Romega_coord_clipped_diff f g n.
rewrite the current goal using Han (from left to right).
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) (Romega_coord_clipped_diff f g n ∈ R)) to the current goal.
Assume Hlt: Rlt (Romega_coord_abs_diff f g n) 1.
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).
An exact proof term for the current goal is HabsDiffR.
Assume Hnlt: ¬ (Rlt (Romega_coord_abs_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).
An exact proof term for the current goal is real_1.
∎