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 ∈ ω.
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 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 Hftot: 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 Hgtot: 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 Hhtot: 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 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 Hftot 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 Hgtot HnO).
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 Hhtot HnO).
We prove the intermediate claim HfnS: SNo (apply_fun f n).
An exact proof term for the current goal is (real_SNo (apply_fun f n) HfnR).
We prove the intermediate claim HgnS: SNo (apply_fun g n).
An exact proof term for the current goal is (real_SNo (apply_fun g n) HgnR).
We prove the intermediate claim HhnS: SNo (apply_fun h n).
An exact proof term for the current goal is (real_SNo (apply_fun h n) HhnR).
Set a to be the term apply_fun f n.
Set b to be the term apply_fun g n.
Set c to be the term apply_fun h n.
We prove the intermediate claim HdefL: Romega_coord_abs_diff f h n = abs_SNo (add_SNo a (minus_SNo c)).
Use reflexivity.
We prove the intermediate claim HdefR1: Romega_coord_abs_diff f g n = abs_SNo (add_SNo a (minus_SNo b)).
Use reflexivity.
We prove the intermediate claim HdefR2: Romega_coord_abs_diff g h n = abs_SNo (add_SNo b (minus_SNo c)).
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).
An exact proof term for the current goal is (abs_SNo_triangle a b c HfnS HgnS HhnS).
∎