Let A, l and eps be given.
Assume Hlub: R_lub A l.
Assume HepsR: eps ∈ R.
Assume HepsPos: Rlt 0 eps.
Set u to be the term add_SNo l (minus_SNo eps).
We prove the intermediate claim HlR: l ∈ R.
An exact proof term for the current goal is (R_lub_in_R A l Hlub).
We prove the intermediate claim HuR: u ∈ R.
An exact proof term for the current goal is (real_add_SNo l HlR (minus_SNo eps) (real_minus_SNo eps HepsR)).
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 HepsS: SNo eps.
An exact proof term for the current goal is (real_SNo eps HepsR).
We prove the intermediate claim HepsPosS: 0 < eps.
An exact proof term for the current goal is (RltE_lt 0 eps HepsPos).
We prove the intermediate claim HmepsR: minus_SNo eps ∈ R.
An exact proof term for the current goal is (real_minus_SNo eps HepsR).
We prove the intermediate claim HmepsS: SNo (minus_SNo eps).
An exact proof term for the current goal is (real_SNo (minus_SNo eps) HmepsR).
We prove the intermediate claim Hmepslt0: minus_SNo eps < 0.
rewrite the current goal using minus_SNo_0 (from right to left).
An exact proof term for the current goal is (minus_SNo_Lt_contra 0 eps SNo_0 HepsS HepsPosS).
We prove the intermediate claim HuLtL: u < l.
We prove the intermediate claim HuDef: u = add_SNo l (minus_SNo eps).
Use reflexivity.
We prove the intermediate claim HuLtL0: add_SNo l (minus_SNo eps) < add_SNo l 0.
An exact proof term for the current goal is (add_SNo_Lt2 l (minus_SNo eps) 0 HlS HmepsS SNo_0 Hmepslt0).
rewrite the current goal using HuDef (from left to right) at position 1.
rewrite the current goal using (add_SNo_0R l HlS) (from right to left) at position 2.
An exact proof term for the current goal is HuLtL0.
We prove the intermediate claim HuLtL_R: Rlt u l.
An exact proof term for the current goal is (RltI u l HuR HlR HuLtL).
We prove the intermediate claim HnotAll: ¬ (∀a : set, a ∈ A → a ∈ R → Rle a u).
Assume Hall: ∀a : set, a ∈ A → a ∈ R → Rle a u.
We prove the intermediate claim Hmin: ∀u0 : set, u0 ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u0) → Rle l u0.
An exact proof term for the current goal is (andER (l ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a l) (∀u0 : set, u0 ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u0) → Rle l u0) Hlub).
We prove the intermediate claim Hle: Rle l u.
An exact proof term for the current goal is (Hmin u HuR Hall).
We prove the intermediate claim Hnlt: ¬ (Rlt u l).
An exact proof term for the current goal is (RleE_nlt l u Hle).
An exact proof term for the current goal is (Hnlt HuLtL_R).
Apply (not_all_ex_demorgan_i (λa : set ⇒ a ∈ A → a ∈ R → Rle a u) HnotAll) to the current goal.
Let a be given.
Assume Hna: ¬ (a ∈ A → a ∈ R → Rle a u).
We prove the intermediate claim Hna1: a ∈ A ∧ ¬ (a ∈ R → Rle a u).
An exact proof term for the current goal is (not_imp (a ∈ A) (a ∈ R → Rle a u) Hna).
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (andEL (a ∈ A) (¬ (a ∈ R → Rle a u)) Hna1).
We prove the intermediate claim Hna2: ¬ (a ∈ R → Rle a u).
An exact proof term for the current goal is (andER (a ∈ A) (¬ (a ∈ R → Rle a u)) Hna1).
We prove the intermediate claim Hna3: a ∈ R ∧ ¬ (Rle a u).
An exact proof term for the current goal is (not_imp (a ∈ R) (Rle a u) Hna2).
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (andEL (a ∈ R) (¬ (Rle a u)) Hna3).
We prove the intermediate claim Hnle: ¬ (Rle a u).
An exact proof term for the current goal is (andER (a ∈ R) (¬ (Rle a u)) Hna3).
We prove the intermediate claim HuLtA: Rlt u a.
Apply (xm (Rlt u a) (Rlt u a)) to the current goal.
Assume Hlt: Rlt u a.
An exact proof term for the current goal is Hlt.
Assume Hnlt: ¬ (Rlt u a).
We prove the intermediate claim Hle: Rle a u.
An exact proof term for the current goal is (RleI a u HaR HuR Hnlt).
An exact proof term for the current goal is (FalseE (Hnle Hle) (Rlt u a)).
We use a to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HaA.
An exact proof term for the current goal is HaR.
An exact proof term for the current goal is HuLtA.
∎