We will prove R_lub {0} 0.
We will prove (0 ∈ R ∧ (∀a : set, a ∈ {0} → a ∈ R → Rle a 0) ∧ (∀u : set, u ∈ R → (∀a : set, a ∈ {0} → a ∈ R → Rle a u) → Rle 0 u)).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is real_0.
Let a be given.
Assume Ha0: a ∈ {0}.
Assume HaR: a ∈ R.
We prove the intermediate claim HaEq: a = 0.
An exact proof term for the current goal is (SingE 0 a Ha0).
rewrite the current goal using HaEq (from left to right).
An exact proof term for the current goal is (Rle_refl 0 real_0).
Let u be given.
Assume HuR: u ∈ R.
Assume Hub: ∀a : set, a ∈ {0} → a ∈ R → Rle a u.
We prove the intermediate claim H0u: Rle 0 u.
An exact proof term for the current goal is (Hub 0 (SingI 0) real_0).
An exact proof term for the current goal is H0u.
∎