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 P to be the term (λr : set ⇒ R_lub A r).
We prove the intermediate claim HAinR: ∀a : set, a ∈ A → a ∈ R.
An exact proof term for the current goal is (Romega_D_scaled_diffs_in_R x y Hx Hy).
We prove the intermediate claim Hub: ∃u : set, u ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a u.
An exact proof term for the current goal is (Romega_D_scaled_diffs_bounded x y Hx Hy).
We prove the intermediate claim HAnen: ∃a0 : set, a0 ∈ A.
We prove the intermediate claim H0omega: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We use (mul_SNo (R_bounded_distance (apply_fun x 0) (apply_fun y 0)) (inv_nat (ordsucc 0))) to witness the existential quantifier.
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 Hex: ∃l : set, P l.
An exact proof term for the current goal is (R_lub_exists A HAnen HAinR Hub).
An exact proof term for the current goal is (Eps_i_ex P Hex).
∎