Let f and g be given.
Assume Hf: f ∈ real_sequences.
Assume Hg: g ∈ real_sequences.
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).
Assume Hl0: Rlt l 0.
We will prove False.
Set a0 to be the term Romega_coord_clipped_diff f g 0.
We prove the intermediate claim H0O: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim Ha0A: a0 ∈ A.
An exact proof term for the current goal is (ReplI ω (λn : set ⇒ Romega_coord_clipped_diff f g n) 0 H0O).
We prove the intermediate claim Ha0R: a0 ∈ R.
An exact proof term for the current goal is (Romega_clipped_diffs_in_R f g Hf Hg a0 Ha0A).
We prove the intermediate claim Ha0S: SNo a0.
An exact proof term for the current goal is (real_SNo a0 Ha0R).
We prove the intermediate claim HlS: SNo l.
An exact proof term for the current goal is (real_SNo l HlR).
We prove the intermediate claim H0S: SNo 0.
An exact proof term for the current goal is SNo_0.
We prove the intermediate claim H0le0: 0 ≤ 0.
An exact proof term for the current goal is (SNoLe_ref 0).
We prove the intermediate claim Ha0nonneg: 0 ≤ a0.
Set t to be the term add_SNo (apply_fun f 0) (minus_SNo (apply_fun g 0)).
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 Hf0R: apply_fun f 0 ∈ R.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y f ω R 0 Htotf H0O).
We prove the intermediate claim Hg0R: apply_fun g 0 ∈ R.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y g ω R 0 Htotg H0O).
We prove the intermediate claim HmfR: minus_SNo (apply_fun g 0) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (apply_fun g 0) Hg0R).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun f 0) Hf0R (minus_SNo (apply_fun g 0)) HmfR).
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 HabsNN: 0 ≤ abs_SNo t.
An exact proof term for the current goal is (abs_SNo_nonneg t HtS).
We prove the intermediate claim HdefAbs: Romega_coord_abs_diff f g 0 = abs_SNo t.
Use reflexivity.
We prove the intermediate claim Hdef: a0 = If_i (Rlt (Romega_coord_abs_diff f g 0) 1) (Romega_coord_abs_diff f g 0) 1.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply (xm (Rlt (Romega_coord_abs_diff f g 0) 1) (0 ≤ (If_i (Rlt (Romega_coord_abs_diff f g 0) 1) (Romega_coord_abs_diff f g 0) 1))) to the current goal.
Assume Hlt: Rlt (Romega_coord_abs_diff f g 0) 1.
rewrite the current goal using (If_i_1 (Rlt (Romega_coord_abs_diff f g 0) 1) (Romega_coord_abs_diff f g 0) 1 Hlt) (from left to right).
rewrite the current goal using HdefAbs (from left to right).
An exact proof term for the current goal is HabsNN.
Assume Hnlt: ¬ (Rlt (Romega_coord_abs_diff f g 0) 1).
rewrite the current goal using (If_i_0 (Rlt (Romega_coord_abs_diff f g 0) 1) (Romega_coord_abs_diff f g 0) 1 Hnlt) (from left to right).
An exact proof term for the current goal is (SNoLtLe 0 1 SNoLt_0_1).
We prove the intermediate claim Ha0lt0n: ¬ (a0 < 0).
We prove the intermediate claim Hcase: 0 < a0 ∨ 0 = a0.
An exact proof term for the current goal is (SNoLeE 0 a0 H0S Ha0S Ha0nonneg).
Assume Ha0lt0: a0 < 0.
Apply (Hcase False) to the current goal.
Assume H0lta0: 0 < a0.
We prove the intermediate claim H00: 0 < 0.
An exact proof term for the current goal is (SNoLt_tra 0 a0 0 H0S Ha0S H0S H0lta0 Ha0lt0).
An exact proof term for the current goal is ((SNoLt_irref 0) H00).
Assume H0eq: 0 = a0.
We prove the intermediate claim H00: 0 < 0.
rewrite the current goal using H0eq (from left to right) at position 1.
An exact proof term for the current goal is Ha0lt0.
An exact proof term for the current goal is ((SNoLt_irref 0) H00).
We prove the intermediate claim Hl0lt: l < 0.
An exact proof term for the current goal is (RltE_lt l 0 Hl0).
We prove the intermediate claim Hlta0: l < a0.
Apply (SNoLt_trichotomy_or_impred a0 0 Ha0S H0S (l < a0)) to the current goal.
Assume Ha0lt0: a0 < 0.
An exact proof term for the current goal is (FalseE (Ha0lt0n Ha0lt0) (l < a0)).
Assume Ha0eq0: a0 = 0.
rewrite the current goal using Ha0eq0 (from left to right).
An exact proof term for the current goal is Hl0lt.
Assume H0lta0: 0 < a0.
An exact proof term for the current goal is (SNoLt_tra l 0 a0 HlS H0S Ha0S Hl0lt H0lta0).
We prove the intermediate claim Hltla0: Rlt l a0.
An exact proof term for the current goal is (RltI l a0 HlR Ha0R Hlta0).
We prove the intermediate claim HRle: Rle a0 l.
An exact proof term for the current goal is (Hub a0 Ha0A Ha0R).
An exact proof term for the current goal is ((RleE_nlt a0 l HRle) Hltla0).
∎