Let x and y be given.
Assume Hx: x ∈ R_omega_space.
Assume Hy: y ∈ R_omega_space.
Assume Hxy0: Romega_D_metric_value x y = 0.
Let i be given.
Assume HiO: i ∈ ω.
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).
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 Hxy0 (from right to left).
An exact proof term for the current goal is (Hub a0 Ha0A Ha0R).
Set bd to be the term R_bounded_distance (apply_fun x i) (apply_fun y i).
Set inv to be the term inv_nat (ordsucc i).
Set a to be the term mul_SNo bd inv.
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (ReplI ω (λj : set ⇒ mul_SNo (R_bounded_distance (apply_fun x j) (apply_fun y j)) (inv_nat (ordsucc j))) i HiO).
We prove the intermediate claim HxiR: apply_fun x i ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R x i Hx HiO).
We prove the intermediate claim HyiR: apply_fun y i ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R y i Hy HiO).
We prove the intermediate claim HbdR: bd ∈ R.
An exact proof term for the current goal is (R_bounded_distance_in_R (apply_fun x i) (apply_fun y i) HxiR HyiR).
We prove the intermediate claim HinvR: inv ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc i) (omega_ordsucc i HiO)).
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (real_mul_SNo bd HbdR inv HinvR).
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 HbdS: SNo bd.
An exact proof term for the current goal is (real_SNo bd HbdR).
We prove the intermediate claim HinvS: SNo inv.
An exact proof term for the current goal is (real_SNo inv HinvR).
We prove the intermediate claim HbdNN: 0 ≤ bd.
An exact proof term for the current goal is (R_bounded_distance_nonneg (apply_fun x i) (apply_fun y i) HxiR HyiR).
We prove the intermediate claim HinvPosR: Rlt 0 inv.
We prove the intermediate claim HsuccO: ordsucc i ∈ ω.
An exact proof term for the current goal is (omega_ordsucc i HiO).
We prove the intermediate claim HsuccNotIn0: ordsucc i ∉ {0}.
Assume Hin0: ordsucc i ∈ {0}.
We prove the intermediate claim Heq: ordsucc i = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc i) Hin0).
An exact proof term for the current goal is (neq_ordsucc_0 i Heq).
We prove the intermediate claim HsuccIn: ordsucc i ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} (ordsucc i) HsuccO HsuccNotIn0).
An exact proof term for the current goal is (inv_nat_pos (ordsucc i) HsuccIn).
We prove the intermediate claim HinvPos: 0 < inv.
An exact proof term for the current goal is (RltE_lt 0 inv HinvPosR).
We prove the intermediate claim HinvNN: 0 ≤ inv.
An exact proof term for the current goal is (SNoLtLe 0 inv HinvPos).
We prove the intermediate claim HaNN: 0 ≤ a.
An exact proof term for the current goal is (mul_SNo_nonneg_nonneg bd inv HbdS HinvS HbdNN HinvNN).
We prove the intermediate claim Ha0: a = 0.
Apply (SNoLeE 0 a SNo_0 (real_SNo a HaR) 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 Hadef: a = mul_SNo bd inv.
Use reflexivity.
We prove the intermediate claim Hbdinv0: mul_SNo bd inv = 0.
rewrite the current goal using Hadef (from right to left).
An exact proof term for the current goal is Ha0.
We prove the intermediate claim HinvNe0: inv ≠ 0.
An exact proof term for the current goal is (SNo_pos_ne0 inv HinvS HinvPos).
We prove the intermediate claim Hinvbd0: mul_SNo inv bd = 0.
rewrite the current goal using (mul_SNo_com inv bd HinvS HbdS) (from left to right) at position 1.
An exact proof term for the current goal is Hbdinv0.
We prove the intermediate claim Hinv0: mul_SNo inv 0 = 0.
An exact proof term for the current goal is (mul_SNo_zeroR inv HinvS).
We prove the intermediate claim Hinvbd_eq: mul_SNo inv bd = mul_SNo inv 0.
rewrite the current goal using Hinvbd0 (from left to right).
rewrite the current goal using Hinv0 (from left to right).
Use reflexivity.
We prove the intermediate claim H0S: SNo 0.
An exact proof term for the current goal is SNo_0.
We prove the intermediate claim Hbd0: bd = 0.
An exact proof term for the current goal is (mul_SNo_nonzero_cancel inv bd 0 HinvS HinvNe0 HbdS H0S Hinvbd_eq).
An exact proof term for the current goal is (R_bounded_distance_eq0 (apply_fun x i) (apply_fun y i) HxiR HyiR Hbd0).
∎