Let f and g be given.
Assume Hf: f ∈ real_sequences.
Assume Hg: g ∈ real_sequences.
Assume Hfg0: Romega_uniform_metric_value f g = 0.
Let n be given.
Assume HnO: n ∈ ω.
Set A to be the term Romega_clipped_diffs f g.
Set l to be the term Romega_uniform_metric_value f g.
We prove the intermediate claim HlR: l ∈ R.
An exact proof term for the current goal is (Romega_uniform_metric_value_in_R f g Hf Hg).
We prove the intermediate claim Hlub: R_lub A l.
An exact proof term for the current goal is (Romega_uniform_metric_value_is_lub f g Hf Hg).
We prove the intermediate claim Hcore: l ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a l.
An exact proof term for the current goal is (andEL (l ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a l) (∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle l u) Hlub).
We prove the intermediate claim Hub: ∀a : set, a ∈ A → a ∈ R → Rle a l.
An exact proof term for the current goal is (andER (l ∈ R) (∀a : set, a ∈ A → a ∈ R → Rle a l) Hcore).
We prove the intermediate claim Hub0: ∀a : set, a ∈ A → a ∈ R → Rle a 0.
Let a0 be given.
Assume Ha0A: a0 ∈ A.
Assume Ha0R: a0 ∈ R.
rewrite the current goal using Hfg0 (from right to left).
An exact proof term for the current goal is (Hub a0 Ha0A Ha0R).
Set a to be the term Romega_coord_clipped_diff f g n.
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (ReplI ω (λm : set ⇒ Romega_coord_clipped_diff f g m) n HnO).
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (Romega_clipped_diffs_in_R f g Hf Hg a HaA).
We prove the intermediate claim HRle: Rle a 0.
An exact proof term for the current goal is (Hub0 a HaA HaR).
We prove the intermediate claim HnRlt0a: ¬ (Rlt 0 a).
An exact proof term for the current goal is (RleE_nlt a 0 HRle).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HaNN: 0 ≤ a.
An exact proof term for the current goal is (Romega_coord_clipped_diff_nonneg f g n Hf Hg HnO).
We prove the intermediate claim Ha0: a = 0.
Apply (SNoLeE 0 a SNo_0 HaS HaNN (a = 0)) to the current goal.
Assume H0lta: 0 < a.
We prove the intermediate claim HRlt0a: Rlt 0 a.
An exact proof term for the current goal is (RltI 0 a real_0 HaR H0lta).
An exact proof term for the current goal is (FalseE (HnRlt0a HRlt0a) (a = 0)).
Assume H0eq: 0 = a.
rewrite the current goal using H0eq (from right to left).
Use reflexivity.
We prove the intermediate claim HfnR: 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 HgnR: 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).
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 Habs0: abs_SNo t = 0.
We prove the intermediate claim HdefAbs: Romega_coord_abs_diff f g n = abs_SNo t.
Use reflexivity.
We prove the intermediate claim HdefClip: a = If_i (Rlt (Romega_coord_abs_diff f g n) 1) (Romega_coord_abs_diff f g n) 1.
Use reflexivity.
We prove the intermediate claim Ha0if: If_i (Rlt (Romega_coord_abs_diff f g n) 1) (Romega_coord_abs_diff f g n) 1 = 0.
rewrite the current goal using HdefClip (from right to left).
An exact proof term for the current goal is Ha0.
Apply (xm (Rlt (Romega_coord_abs_diff f g n) 1) (abs_SNo t = 0)) to the current goal.
Assume Hlt: Rlt (Romega_coord_abs_diff f g n) 1.
We prove the intermediate claim Hif: If_i (Rlt (Romega_coord_abs_diff f g n) 1) (Romega_coord_abs_diff f g n) 1 = (Romega_coord_abs_diff f g n).
An exact proof term for the current goal is (If_i_1 (Rlt (Romega_coord_abs_diff f g n) 1) (Romega_coord_abs_diff f g n) 1 Hlt).
We prove the intermediate claim HabsR0: Romega_coord_abs_diff f g n = 0.
rewrite the current goal using Hif (from right to left).
An exact proof term for the current goal is Ha0if.
rewrite the current goal using HdefAbs (from right to left).
An exact proof term for the current goal is HabsR0.
Assume Hnlt: ¬ (Rlt (Romega_coord_abs_diff f g n) 1).
We prove the intermediate claim Hif: If_i (Rlt (Romega_coord_abs_diff f g n) 1) (Romega_coord_abs_diff f g n) 1 = 1.
An exact proof term for the current goal is (If_i_0 (Rlt (Romega_coord_abs_diff f g n) 1) (Romega_coord_abs_diff f g n) 1 Hnlt).
We prove the intermediate claim H10eq: 1 = 0.
rewrite the current goal using Hif (from right to left).
An exact proof term for the current goal is Ha0if.
An exact proof term for the current goal is (FalseE ((neq_1_0) H10eq) (abs_SNo t = 0)).
We prove the intermediate claim Ht0: t = 0.
Apply (xm (0 ≤ t) (t = 0)) to the current goal.
Assume H0le: 0 ≤ t.
rewrite the current goal using (nonneg_abs_SNo t H0le) (from right to left).
An exact proof term for the current goal is Habs0.
Assume Hn0le: ¬ (0 ≤ t).
We prove the intermediate claim Hm0: minus_SNo t = 0.
rewrite the current goal using (not_nonneg_abs_SNo t Hn0le) (from right to left).
An exact proof term for the current goal is Habs0.
We prove the intermediate claim Hsum: add_SNo (minus_SNo t) t = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_linv t HtS).
We prove the intermediate claim H0t0: add_SNo 0 t = 0.
rewrite the current goal using Hm0 (from right to left) at position 1.
An exact proof term for the current goal is Hsum.
rewrite the current goal using (add_SNo_0L t HtS) (from right to left).
An exact proof term for the current goal is H0t0.
We prove the intermediate claim Htdef: t = add_SNo (apply_fun f n) (minus_SNo (apply_fun g n)).
Use reflexivity.
We prove the intermediate claim Ht0': add_SNo (apply_fun f n) (minus_SNo (apply_fun g n)) = 0.
rewrite the current goal using Htdef (from right to left).
An exact proof term for the current goal is Ht0.
We prove the intermediate claim Hrhs0: add_SNo (apply_fun g n) (minus_SNo (apply_fun g n)) = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv (apply_fun g n) (real_SNo (apply_fun g n) HgnR)).
We prove the intermediate claim Heq: add_SNo (apply_fun f n) (minus_SNo (apply_fun g n)) = add_SNo (apply_fun g n) (minus_SNo (apply_fun g n)).
rewrite the current goal using Ht0' (from left to right) at position 1.
rewrite the current goal using Hrhs0 (from left to right) at position 1.
Use reflexivity.
An exact proof term for the current goal is (add_SNo_cancel_R (apply_fun f n) (minus_SNo (apply_fun g n)) (apply_fun g n) (real_SNo (apply_fun f n) HfnR) (SNo_minus_SNo (apply_fun g n) (real_SNo (apply_fun g n) HgnR)) (real_SNo (apply_fun g n) HgnR) Heq).
∎