Let A be given.
Assume HAnen: ∃a0 : set, a0 ∈ A.
Assume HAinR: ∀a : set, a ∈ A → a ∈ R.
Assume HubExists: ∃u : set, u ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a u.
Set L to be the term {x ∈ R|∃a ∈ A, Rlt x a}.
Set U to be the term {u ∈ R|∀a : set, a ∈ A → a ∈ R → Rle a u}.
Set Rplus to be the term {y ∈ R|∃u ∈ U, ∃n ∈ ω, y = add_SNo u (eps_ n)}.
We prove the intermediate claim HLsub: L ⊆ real.
Let x be given.
Assume HxL: x ∈ L.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ ∃a ∈ A, Rlt x0 a) x HxL).
We prove the intermediate claim HRsub: Rplus ⊆ real.
Let y be given.
Assume Hy: y ∈ Rplus.
An exact proof term for the current goal is (SepE1 R (λy0 : set ⇒ ∃u ∈ U, ∃n ∈ ω, y0 = add_SNo u (eps_ n)) y Hy).
We prove the intermediate claim HU_nonempty: ∃u0 : set, u0 ∈ U.
Apply HubExists to the current goal.
Let u0 be given.
Assume Hu0pack: u0 ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a u0.
We use u0 to witness the existential quantifier.
Apply (SepI R (λu : set ⇒ ∀a : set, a ∈ A → a ∈ R → Rle a u) u0) to the current goal.
An exact proof term for the current goal is (andEL (u0 ∈ R) (∀a : set, a ∈ A → a ∈ R → Rle a u0) Hu0pack).
An exact proof term for the current goal is (andER (u0 ∈ R) (∀a : set, a ∈ A → a ∈ R → Rle a u0) Hu0pack).
We prove the intermediate claim HLne: L ≠ 0.
Apply HAnen to the current goal.
Let a0 be given.
Assume Ha0A: a0 ∈ A.
We prove the intermediate claim Ha0R: a0 ∈ R.
An exact proof term for the current goal is (HAinR a0 Ha0A).
Set x0 to be the term add_SNo a0 (minus_SNo 1).
We prove the intermediate claim Hx0R: x0 ∈ R.
An exact proof term for the current goal is (real_add_SNo a0 Ha0R (minus_SNo 1) (real_minus_SNo 1 real_1)).
We prove the intermediate claim Hx0S: SNo x0.
An exact proof term for the current goal is (real_SNo x0 Hx0R).
We prove the intermediate claim Hx0Def: x0 = add_SNo a0 (minus_SNo 1).
Use reflexivity.
We prove the intermediate claim Hx0lt_a0: x0 < a0.
We prove the intermediate claim Hx0eps: x0 < add_SNo x0 (eps_ 0).
An exact proof term for the current goal is (add_SNo_eps_Lt x0 Hx0S 0 (nat_p_omega 0 nat_0)).
We prove the intermediate claim Hx0plusEps: add_SNo x0 (eps_ 0) = a0.
rewrite the current goal using (eps_0_1) (from left to right) at position 1.
rewrite the current goal using Hx0Def (from left to right) at position 1.
An exact proof term for the current goal is (add_SNo_minus_R2' a0 1 (real_SNo a0 Ha0R) SNo_1).
rewrite the current goal using Hx0plusEps (from right to left) at position 2.
An exact proof term for the current goal is Hx0eps.
We prove the intermediate claim Hx0lt: Rlt x0 a0.
An exact proof term for the current goal is (RltI x0 a0 Hx0R Ha0R Hx0lt_a0).
We prove the intermediate claim Hx0inL: x0 ∈ L.
Apply (SepI R (λx : set ⇒ ∃a ∈ A, Rlt x a) x0 Hx0R) to the current goal.
We use a0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0A.
An exact proof term for the current goal is Hx0lt.
Assume Hz: L = 0.
We prove the intermediate claim Hx0notL: x0 ∉ L.
rewrite the current goal using Hz (from left to right).
An exact proof term for the current goal is (EmptyE x0).
An exact proof term for the current goal is (Hx0notL Hx0inL).
We prove the intermediate claim HRne: Rplus ≠ 0.
Apply HU_nonempty to the current goal.
Let u0 be given.
Assume Hu0U: u0 ∈ U.
We prove the intermediate claim Hu0R: u0 ∈ R.
An exact proof term for the current goal is (SepE1 R (λu : set ⇒ ∀a : set, a ∈ A → a ∈ R → Rle a u) u0 Hu0U).
We prove the intermediate claim Heps0R: eps_ 0 ∈ R.
rewrite the current goal using (eps_0_1) (from left to right).
An exact proof term for the current goal is real_1.
Set y0 to be the term add_SNo u0 (eps_ 0).
We prove the intermediate claim Hy0R: y0 ∈ R.
An exact proof term for the current goal is (real_add_SNo u0 Hu0R (eps_ 0) Heps0R).
We prove the intermediate claim Hy0in: y0 ∈ Rplus.
Apply (SepI R (λy : set ⇒ ∃u ∈ U, ∃n ∈ ω, y = add_SNo u (eps_ n)) y0 Hy0R) to the current goal.
We use u0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hu0U.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
Use reflexivity.
Assume H0: Rplus = 0.
We prove the intermediate claim Hy0notR: y0 ∉ Rplus.
rewrite the current goal using H0 (from left to right).
An exact proof term for the current goal is (EmptyE y0).
An exact proof term for the current goal is (Hy0notR Hy0in).
We prove the intermediate claim HLnoMax: ∀w ∈ L, ∃w' ∈ L, w < w'.
Let w be given.
Assume HwL: w ∈ L.
We prove the intermediate claim HwR: w ∈ R.
An exact proof term for the current goal is (SepE1 R (λx : set ⇒ ∃a ∈ A, Rlt x a) w HwL).
We prove the intermediate claim Hexa: ∃a : set, a ∈ A ∧ Rlt w a.
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ ∃a ∈ A, Rlt x a) w HwL).
Apply Hexa to the current goal.
Let a be given.
Assume Hapack: a ∈ A ∧ Rlt w a.
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (andEL (a ∈ A) (Rlt w a) Hapack).
We prove the intermediate claim Hwa: Rlt w a.
An exact proof term for the current goal is (andER (a ∈ A) (Rlt w a) Hapack).
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (HAinR a HaA).
We prove the intermediate claim Hexq: ∃q ∈ rational_numbers, Rlt w q ∧ Rlt q a.
An exact proof term for the current goal is (rational_dense_between_reals w a HwR HaR Hwa).
Apply Hexq to the current goal.
Let q be given.
Assume Hqpack: q ∈ rational_numbers ∧ (Rlt w q ∧ Rlt q a).
We prove the intermediate claim HqQ: q ∈ rational_numbers.
An exact proof term for the current goal is (andEL (q ∈ rational_numbers) (Rlt w q ∧ Rlt q a) Hqpack).
We prove the intermediate claim Hqmid: Rlt w q ∧ Rlt q a.
An exact proof term for the current goal is (andER (q ∈ rational_numbers) (Rlt w q ∧ Rlt q a) Hqpack).
We prove the intermediate claim Hwq: Rlt w q.
An exact proof term for the current goal is (andEL (Rlt w q) (Rlt q a) Hqmid).
We prove the intermediate claim Hqa: Rlt q a.
An exact proof term for the current goal is (andER (Rlt w q) (Rlt q a) Hqmid).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We use q to witness the existential quantifier.
Apply andI to the current goal.
Apply (SepI R (λx : set ⇒ ∃a0 ∈ A, Rlt x a0) q HqR) to the current goal.
We use a to witness the existential quantifier.
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 Hqa.
An exact proof term for the current goal is (RltE_lt w q Hwq).
We prove the intermediate claim HRnoMin: ∀z ∈ Rplus, ∃z' ∈ Rplus, z' < z.
Let z be given.
Assume HzR: z ∈ Rplus.
We prove the intermediate claim HzR0: z ∈ R.
An exact proof term for the current goal is (SepE1 R (λy : set ⇒ ∃u ∈ U, ∃n ∈ ω, y = add_SNo u (eps_ n)) z HzR).
We prove the intermediate claim Hex: ∃u : set, u ∈ U ∧ ∃n : set, n ∈ ω ∧ z = add_SNo u (eps_ n).
An exact proof term for the current goal is (SepE2 R (λy : set ⇒ ∃u ∈ U, ∃n ∈ ω, y = add_SNo u (eps_ n)) z HzR).
Apply Hex to the current goal.
Let u be given.
Assume Hun.
We prove the intermediate claim HuU: u ∈ U.
An exact proof term for the current goal is (andEL (u ∈ U) (∃n : set, n ∈ ω ∧ z = add_SNo u (eps_ n)) Hun).
We prove the intermediate claim Hexn: ∃n : set, n ∈ ω ∧ z = add_SNo u (eps_ n).
An exact proof term for the current goal is (andER (u ∈ U) (∃n : set, n ∈ ω ∧ z = add_SNo u (eps_ n)) Hun).
Apply Hexn to the current goal.
Let n be given.
Assume Hnpack: n ∈ ω ∧ z = add_SNo u (eps_ n).
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (andEL (n ∈ ω) (z = add_SNo u (eps_ n)) Hnpack).
We prove the intermediate claim Hzdef: z = add_SNo u (eps_ n).
An exact proof term for the current goal is (andER (n ∈ ω) (z = add_SNo u (eps_ n)) Hnpack).
Set n1 to be the term ordsucc n.
We prove the intermediate claim Hn1O: n1 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n HnO).
We prove the intermediate claim HuR: u ∈ R.
An exact proof term for the current goal is (SepE1 R (λu0 : set ⇒ ∀a : set, a ∈ A → a ∈ R → Rle a u0) u HuU).
We prove the intermediate claim HuS: SNo u.
An exact proof term for the current goal is (real_SNo u HuR).
We prove the intermediate claim HepsnS: SNo (eps_ n).
An exact proof term for the current goal is (SNo_eps_ n HnO).
We prove the intermediate claim Hepsn1S: SNo (eps_ n1).
An exact proof term for the current goal is (SNo_eps_ n1 Hn1O).
We prove the intermediate claim Hnin: n ∈ n1.
An exact proof term for the current goal is (ordsuccI2 n).
We prove the intermediate claim Hepsdec: eps_ n1 < eps_ n.
An exact proof term for the current goal is (SNo_eps_decr n1 Hn1O n Hnin).
Set z1 to be the term add_SNo u (eps_ n1).
We prove the intermediate claim Hz1R: z1 ∈ R.
An exact proof term for the current goal is (real_add_SNo u HuR (eps_ n1) (SNoS_omega_real (eps_ n1) (SNo_eps_SNoS_omega n1 Hn1O))).
We prove the intermediate claim Hz1in: z1 ∈ Rplus.
Apply (SepI R (λy : set ⇒ ∃u0 ∈ U, ∃k ∈ ω, y = add_SNo u0 (eps_ k)) z1 Hz1R) to the current goal.
We use u to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HuU.
We use n1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn1O.
Use reflexivity.
We use z1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz1in.
rewrite the current goal using Hzdef (from left to right).
An exact proof term for the current goal is (add_SNo_Lt2 u (eps_ n1) (eps_ n) HuS Hepsn1S HepsnS Hepsdec).
We prove the intermediate claim HcutP: SNoCutP L Rplus.
We will prove (∀x ∈ L, SNo x) ∧ (∀y ∈ Rplus, SNo y) ∧ (∀x ∈ L, ∀y ∈ Rplus, x < y).
Apply and3I to the current goal.
Let x be given.
Assume HxL: x ∈ L.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ ∃a ∈ A, Rlt x0 a) x HxL).
An exact proof term for the current goal is (real_SNo x HxR).
Let y be given.
Assume HyR: y ∈ Rplus.
We prove the intermediate claim HyRR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λy0 : set ⇒ ∃u ∈ U, ∃n ∈ ω, y0 = add_SNo u (eps_ n)) y HyR).
An exact proof term for the current goal is (real_SNo y HyRR).
Let x be given.
Assume HxL: x ∈ L.
Let y be given.
Assume HyR: y ∈ Rplus.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ ∃a ∈ A, Rlt x0 a) x HxL).
We prove the intermediate claim HyRR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λy0 : set ⇒ ∃u ∈ U, ∃n ∈ ω, y0 = add_SNo u (eps_ n)) y HyR).
We prove the intermediate claim Hexa: ∃a : set, a ∈ A ∧ Rlt x a.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ∃a ∈ A, Rlt x0 a) x HxL).
Apply Hexa to the current goal.
Let a be given.
Assume Hapack: a ∈ A ∧ Rlt x a.
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (andEL (a ∈ A) (Rlt x a) Hapack).
We prove the intermediate claim Hxa: Rlt x a.
An exact proof term for the current goal is (andER (a ∈ A) (Rlt x a) Hapack).
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (HAinR a HaA).
We prove the intermediate claim Hexun: ∃u : set, u ∈ U ∧ ∃n : set, n ∈ ω ∧ y = add_SNo u (eps_ n).
An exact proof term for the current goal is (SepE2 R (λy0 : set ⇒ ∃u ∈ U, ∃n ∈ ω, y0 = add_SNo u (eps_ n)) y HyR).
Apply Hexun to the current goal.
Let u be given.
Assume Hun.
We prove the intermediate claim HuU: u ∈ U.
An exact proof term for the current goal is (andEL (u ∈ U) (∃n : set, n ∈ ω ∧ y = add_SNo u (eps_ n)) Hun).
We prove the intermediate claim Hexn: ∃n : set, n ∈ ω ∧ y = add_SNo u (eps_ n).
An exact proof term for the current goal is (andER (u ∈ U) (∃n : set, n ∈ ω ∧ y = add_SNo u (eps_ n)) Hun).
Apply Hexn to the current goal.
Let n be given.
Assume Hnpack: n ∈ ω ∧ y = add_SNo u (eps_ n).
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (andEL (n ∈ ω) (y = add_SNo u (eps_ n)) Hnpack).
We prove the intermediate claim Hydef: y = add_SNo u (eps_ n).
An exact proof term for the current goal is (andER (n ∈ ω) (y = add_SNo u (eps_ n)) Hnpack).
We prove the intermediate claim HuR: u ∈ R.
An exact proof term for the current goal is (SepE1 R (λu0 : set ⇒ ∀a0 : set, a0 ∈ A → a0 ∈ R → Rle a0 u0) u HuU).
We prove the intermediate claim HuS: SNo u.
An exact proof term for the current goal is (real_SNo u HuR).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim HepsnS: SNo (eps_ n).
An exact proof term for the current goal is (SNo_eps_ n HnO).
We prove the intermediate claim Hxa_lt: x < a.
An exact proof term for the current goal is (RltE_lt x a Hxa).
We prove the intermediate claim Hau_nlt: ¬ (Rlt u a).
An exact proof term for the current goal is (RleE_nlt a u ((SepE2 R (λu0 : set ⇒ ∀a0 : set, a0 ∈ A → a0 ∈ R → Rle a0 u0) u HuU) a HaA HaR)).
We prove the intermediate claim Hxltu: x < u.
Apply (SNoLt_trichotomy_or_impred u a HuS HaS (x < u)) to the current goal.
Assume Hult: u < a.
We prove the intermediate claim HultR: Rlt u a.
An exact proof term for the current goal is (RltI u a HuR HaR Hult).
An exact proof term for the current goal is (FalseE (Hau_nlt HultR) (x < u)).
Assume Hueq: u = a.
rewrite the current goal using Hueq (from left to right).
An exact proof term for the current goal is Hxa_lt.
Assume Halt: a < u.
An exact proof term for the current goal is (SNoLt_tra x a u HxS HaS HuS Hxa_lt Halt).
We prove the intermediate claim Hultup: u < add_SNo u (eps_ n).
An exact proof term for the current goal is (add_SNo_eps_Lt u HuS n HnO).
rewrite the current goal using Hydef (from left to right).
An exact proof term for the current goal is (SNoLt_tra x u (add_SNo u (eps_ n)) HxS HuS (real_SNo (add_SNo u (eps_ n)) (real_add_SNo u HuR (eps_ n) (SNoS_omega_real (eps_ n) (SNo_eps_SNoS_omega n HnO)))) Hxltu Hultup).
Set l to be the term SNoCut L Rplus.
We prove the intermediate claim HlR: l ∈ R.
An exact proof term for the current goal is (real_SNoCut L HLsub Rplus HRsub HcutP HLne HRne HLnoMax HRnoMin).
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 Hbelow: ∀x ∈ L, x < l.
An exact proof term for the current goal is (SNoCutP_SNoCut_L L Rplus HcutP).
We prove the intermediate claim Habove: ∀y ∈ Rplus, l < y.
An exact proof term for the current goal is (SNoCutP_SNoCut_R L Rplus HcutP).
We use l to witness the existential quantifier.
We will prove R_lub A l.
We will prove (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).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HlR.
Let a be given.
Assume HaA: a ∈ A.
Assume HaR: a ∈ R.
We will prove Rle a l.
Apply (RleI a l HaR HlR) to the current goal.
Assume Hlt: Rlt l a.
We prove the intermediate claim HlinL: l ∈ L.
Apply (SepI R (λx : set ⇒ ∃a0 ∈ A, Rlt x a0) l HlR) to the current goal.
We use a to witness the existential quantifier.
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 Hlt.
We prove the intermediate claim Hll: l < l.
An exact proof term for the current goal is (Hbelow l HlinL).
An exact proof term for the current goal is ((SNoLt_irref l) Hll).
Let u be given.
Assume HuR: u ∈ R.
Assume Hupper: ∀a : set, a ∈ A → a ∈ R → Rle a u.
We will prove Rle l u.
Apply (RleI l u HlR HuR) to the current goal.
Assume Hult: Rlt u l.
Set d to be the term add_SNo l (minus_SNo u).
We prove the intermediate claim HdR: d ∈ R.
An exact proof term for the current goal is (real_add_SNo l HlR (minus_SNo u) (real_minus_SNo u HuR)).
We prove the intermediate claim Hdpos: Rlt 0 d.
An exact proof term for the current goal is (Rlt_0_diff_of_lt u l Hult).
We prove the intermediate claim HexN: ∃N ∈ ω, eps_ N < d.
An exact proof term for the current goal is (exists_eps_lt_pos d HdR Hdpos).
Apply HexN to the current goal.
Let N be given.
Assume HNpack.
We prove the intermediate claim HNomega: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (eps_ N < d) HNpack).
We prove the intermediate claim HepsNd: eps_ N < d.
An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < d) HNpack).
We prove the intermediate claim HuS: SNo u.
An exact proof term for the current goal is (real_SNo u HuR).
We prove the intermediate claim HdS: SNo d.
An exact proof term for the current goal is (real_SNo d HdR).
We prove the intermediate claim HepsNS: SNo (eps_ N).
An exact proof term for the current goal is (SNo_eps_ N HNomega).
Set y to be the term add_SNo u (eps_ N).
We prove the intermediate claim HepsNR: eps_ N ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ N) (SNo_eps_SNoS_omega N HNomega)).
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (real_add_SNo u HuR (eps_ N) HepsNR).
We prove the intermediate claim HuU: u ∈ U.
An exact proof term for the current goal is (SepI R (λu0 : set ⇒ ∀a0 : set, a0 ∈ A → a0 ∈ R → Rle a0 u0) u HuR Hupper).
We prove the intermediate claim Hyin: y ∈ Rplus.
Apply (SepI R (λy0 : set ⇒ ∃u0 ∈ U, ∃n ∈ ω, y0 = add_SNo u0 (eps_ n)) y HyR) to the current goal.
We use u to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HuU.
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HNomega.
Use reflexivity.
We prove the intermediate claim Hyltuplusd: add_SNo u (eps_ N) < add_SNo u d.
An exact proof term for the current goal is (add_SNo_Lt2 u (eps_ N) d HuS HepsNS HdS HepsNd).
We prove the intermediate claim Hdcomm: d = add_SNo (minus_SNo u) l.
We prove the intermediate claim HmuS: SNo (minus_SNo u).
An exact proof term for the current goal is (SNo_minus_SNo u HuS).
An exact proof term for the current goal is (add_SNo_com l (minus_SNo u) HlS HmuS).
We prove the intermediate claim Huplusd: add_SNo u d = l.
We prove the intermediate claim HmuR: minus_SNo u ∈ R.
An exact proof term for the current goal is (real_minus_SNo u HuR).
We prove the intermediate claim HmuS: SNo (minus_SNo u).
An exact proof term for the current goal is (real_SNo (minus_SNo u) HmuR).
rewrite the current goal using Hdcomm (from left to right).
An exact proof term for the current goal is (add_SNo_minus_L2' u l HuS HlS).
We prove the intermediate claim Hyltl: y < l.
rewrite the current goal using Huplusd (from right to left).
An exact proof term for the current goal is Hyltuplusd.
We prove the intermediate claim Hlty: l < y.
An exact proof term for the current goal is (Habove y Hyin).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim Hbad: y < y.
An exact proof term for the current goal is (SNoLt_tra y l y HyS HlS HyS Hyltl Hlty).
An exact proof term for the current goal is ((SNoLt_irref y) Hbad).
∎