Let f, g and n be given.
Assume Hf: f ∈ real_sequences.
Assume Hg: g ∈ real_sequences.
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).
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 HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
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.
rewrite the current goal using (nonneg_abs_SNo t H0le) (from left to right).
An exact proof term for the current goal is HtR.
Assume Hn0le: ¬ (0 ≤ t).
rewrite the current goal using (not_nonneg_abs_SNo t Hn0le) (from left to right).
An exact proof term for the current goal is (real_minus_SNo t HtR).
We prove the intermediate claim Hdef: Romega_coord_abs_diff f g n = abs_SNo t.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is HabsR.
∎