Let x, y and 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 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).

Set a to be the term mul_SNo (R_bounded_distance (apply_fun x i) (apply_fun y i)) (inv_nat (ordsucc i)).

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: R_bounded_distance (apply_fun x i) (apply_fun y i) ∈ 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 HsuccO: ordsucc i ∈ ω.

An exact proof term for the current goal is (omega_ordsucc i HiO).

We prove the intermediate claim HinvR: inv_nat (ordsucc i) ∈ R.

An exact proof term for the current goal is (inv_nat_real (ordsucc i) HsuccO).

We prove the intermediate claim HaR: a ∈ R.

An exact proof term for the current goal is (real_mul_SNo (R_bounded_distance (apply_fun x i) (apply_fun y i)) HbdR (inv_nat (ordsucc i)) HinvR).

An exact proof term for the current goal is (Hub a HaA HaR).

∎