Let x and y be given.
Assume Hx: x ∈ R_omega_space.
Assume Hy: y ∈ R_omega_space.
Set A to be the term Romega_D_scaled_diffs x y.
Set l to be the term Romega_D_metric_value x y.
We prove the intermediate claim HlR: l ∈ R.
An exact proof term for the current goal is (Romega_D_metric_value_in_R x y Hx Hy).
We prove the intermediate claim Hlub: R_lub A l.
An exact proof term for the current goal is (Romega_D_metric_value_is_lub x y Hx Hy).
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 a1 to be the term mul_SNo (R_bounded_distance (apply_fun x 0) (apply_fun y 0)) (inv_nat (ordsucc 0)).
We prove the intermediate claim H0omega: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim Ha1A: a1 ∈ A.
An exact proof term for the current goal is (ReplI ω (λi : set ⇒ mul_SNo (R_bounded_distance (apply_fun x i) (apply_fun y i)) (inv_nat (ordsucc i))) 0 H0omega).
We prove the intermediate claim HxiR: apply_fun x 0 ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R x 0 Hx H0omega).
We prove the intermediate claim HyiR: apply_fun y 0 ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R y 0 Hy H0omega).
We prove the intermediate claim HbdR: R_bounded_distance (apply_fun x 0) (apply_fun y 0) ∈ R.
An exact proof term for the current goal is (R_bounded_distance_in_R (apply_fun x 0) (apply_fun y 0) HxiR HyiR).
We prove the intermediate claim H1omega: ordsucc 0 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc 0 H0omega).
We prove the intermediate claim H1not0: ordsucc 0 ∉ {0}.
Assume H1: ordsucc 0 ∈ {0}.
We prove the intermediate claim Heq: ordsucc 0 = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc 0) H1).
An exact proof term for the current goal is (neq_ordsucc_0 0 Heq).
We prove the intermediate claim H1In: ordsucc 0 ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} (ordsucc 0) H1omega H1not0).
We prove the intermediate claim HinvR: inv_nat (ordsucc 0) ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc 0) H1omega).
We prove the intermediate claim Ha1R: a1 ∈ R.
An exact proof term for the current goal is (real_mul_SNo (R_bounded_distance (apply_fun x 0) (apply_fun y 0)) HbdR (inv_nat (ordsucc 0)) HinvR).
We prove the intermediate claim Ha1S: SNo a1.
An exact proof term for the current goal is (real_SNo a1 Ha1R).
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 HbdS: SNo (R_bounded_distance (apply_fun x 0) (apply_fun y 0)).
An exact proof term for the current goal is (real_SNo (R_bounded_distance (apply_fun x 0) (apply_fun y 0)) HbdR).
We prove the intermediate claim HinvS: SNo (inv_nat (ordsucc 0)).
An exact proof term for the current goal is (real_SNo (inv_nat (ordsucc 0)) HinvR).
We prove the intermediate claim HbdNN: 0 ≤ R_bounded_distance (apply_fun x 0) (apply_fun y 0).
An exact proof term for the current goal is (R_bounded_distance_nonneg (apply_fun x 0) (apply_fun y 0) HxiR HyiR).
We prove the intermediate claim HinvPosR: Rlt 0 (inv_nat (ordsucc 0)).
An exact proof term for the current goal is (inv_nat_pos (ordsucc 0) H1In).
We prove the intermediate claim HinvPos: 0 < inv_nat (ordsucc 0).
An exact proof term for the current goal is (RltE_lt 0 (inv_nat (ordsucc 0)) HinvPosR).
We prove the intermediate claim HinvNN: 0 ≤ inv_nat (ordsucc 0).
An exact proof term for the current goal is (SNoLtLe 0 (inv_nat (ordsucc 0)) HinvPos).
We prove the intermediate claim Ha1nonneg: 0 ≤ a1.
An exact proof term for the current goal is (mul_SNo_nonneg_nonneg (R_bounded_distance (apply_fun x 0) (apply_fun y 0)) (inv_nat (ordsucc 0)) HbdS HinvS HbdNN HinvNN).
We prove the intermediate claim Ha1lt0n: ¬ (a1 < 0).
We prove the intermediate claim Hcase: 0 < a1 ∨ 0 = a1.
An exact proof term for the current goal is (SNoLeE 0 a1 H0S Ha1S Ha1nonneg).
Assume Ha1lt0: a1 < 0.
Apply (Hcase False) to the current goal.
Assume H0lta1: 0 < a1.
We prove the intermediate claim H00: 0 < 0.
An exact proof term for the current goal is (SNoLt_tra 0 a1 0 H0S Ha1S H0S H0lta1 Ha1lt0).
An exact proof term for the current goal is ((SNoLt_irref 0) H00).
Assume H0eq: 0 = a1.
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 Ha1lt0.
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 Hlta1: l < a1.
Apply (SNoLt_trichotomy_or_impred a1 0 Ha1S H0S (l < a1)) to the current goal.
Assume Ha1lt0: a1 < 0.
An exact proof term for the current goal is (FalseE (Ha1lt0n Ha1lt0) (l < a1)).
Assume Ha1eq0: a1 = 0.
rewrite the current goal using Ha1eq0 (from left to right).
An exact proof term for the current goal is Hl0lt.
Assume H0lta1: 0 < a1.
An exact proof term for the current goal is (SNoLt_tra l 0 a1 HlS H0S Ha1S Hl0lt H0lta1).
We prove the intermediate claim Hltla1: Rlt l a1.
An exact proof term for the current goal is (RltI l a1 HlR Ha1R Hlta1).
We prove the intermediate claim HRle: Rle a1 l.
An exact proof term for the current goal is (Hub a1 Ha1A Ha1R).
An exact proof term for the current goal is ((RleE_nlt a1 l HRle) Hltla1).
∎