Let b be given.
Assume HbR: b ∈ R.
Assume Hbpos: Rlt 0 b.
We will prove finite (K_set ∩ {y ∈ R|Rlt b y}).
Set V to be the term {y ∈ R|Rlt b y}.
Set r to be the term recip_SNo b.
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim H0ltb: 0 < b.
An exact proof term for the current goal is (RltE_lt 0 b Hbpos).
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (SNo_recip_SNo b HbS).
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (real_recip_SNo b HbR).
We prove the intermediate claim Hrpos: 0 < r.
An exact proof term for the current goal is (recip_SNo_of_pos_is_pos b HbS H0ltb).
We prove the intermediate claim Hrnonneg: 0 ≤ r.
An exact proof term for the current goal is (SNoLtLe 0 r Hrpos).
We prove the intermediate claim Hexn: ∃n ∈ ω, n ≤ r ∧ r < ordsucc n.
An exact proof term for the current goal is (nonneg_real_nat_interval r HrR Hrnonneg).
Apply Hexn to the current goal.
Let n be given.
Assume Hnpair.
We prove the intermediate claim HnOmega: n ∈ ω.
An exact proof term for the current goal is (andEL (n ∈ ω) (n ≤ r ∧ r < ordsucc n) Hnpair).
We prove the intermediate claim Hnrest: n ≤ r ∧ r < ordsucc n.
An exact proof term for the current goal is (andER (n ∈ ω) (n ≤ r ∧ r < ordsucc n) Hnpair).
We prove the intermediate claim HrltN: r < ordsucc n.
An exact proof term for the current goal is (andER (n ≤ r) (r < ordsucc n) Hnrest).
Set N to be the term ordsucc n.
We prove the intermediate claim HNOmega: N ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n HnOmega).
We prove the intermediate claim HNS: SNo N.
An exact proof term for the current goal is (omega_SNo N HNOmega).
We prove the intermediate claim HNNat: nat_p N.
An exact proof term for the current goal is (omega_nat_p N HNOmega).
We prove the intermediate claim HNOrd: ordinal N.
An exact proof term for the current goal is (nat_p_ordinal N HNNat).
We prove the intermediate claim HNfin: finite N.
An exact proof term for the current goal is (nat_finite N HNNat).
Set I to be the term N ∖ {0}.
We prove the intermediate claim HIfin: finite I.
An exact proof term for the current goal is (Subq_finite N HNfin I (setminus_Subq N {0})).
Set Big to be the term {inv_nat m|m ∈ I}.
We prove the intermediate claim HBigFin: finite Big.
An exact proof term for the current goal is (Repl_finite (λm : set ⇒ inv_nat m) I HIfin).
We prove the intermediate claim Hsub: K_set ∩ V ⊆ Big.
Let x be given.
Assume Hx: x ∈ K_set ∩ V.
We will prove x ∈ Big.
We prove the intermediate claim HxK: x ∈ K_set.
An exact proof term for the current goal is (binintersectE1 K_set V x Hx).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE2 K_set V x Hx).
Apply (ReplE (ω ∖ {0}) (λm : set ⇒ inv_nat m) x HxK) to the current goal.
Let m be given.
Assume Hmconj.
We prove the intermediate claim HmIn: m ∈ ω ∖ {0}.
An exact proof term for the current goal is (andEL (m ∈ ω ∖ {0}) (x = inv_nat m) Hmconj).
We prove the intermediate claim Hxeq: x = inv_nat m.
An exact proof term for the current goal is (andER (m ∈ ω ∖ {0}) (x = inv_nat m) Hmconj).
rewrite the current goal using Hxeq (from left to right).
We prove the intermediate claim HmOmega: m ∈ ω.
An exact proof term for the current goal is (setminusE1 ω {0} m HmIn).
We prove the intermediate claim Hmnot0: m ∉ {0}.
An exact proof term for the current goal is (setminusE2 ω {0} m HmIn).
We prove the intermediate claim HmS: SNo m.
An exact proof term for the current goal is (omega_SNo m HmOmega).
We prove the intermediate claim HmNat: nat_p m.
An exact proof term for the current goal is (omega_nat_p m HmOmega).
We prove the intermediate claim HmOrd: ordinal m.
An exact proof term for the current goal is (nat_p_ordinal m HmNat).
We prove the intermediate claim Hmne0: m ≠ 0.
Assume Hm0: m = 0.
We prove the intermediate claim Hmin0: m ∈ {0}.
rewrite the current goal using Hm0 (from left to right).
An exact proof term for the current goal is (SingI 0).
An exact proof term for the current goal is (Hmnot0 Hmin0).
We prove the intermediate claim Hmcase: m = 0 ∨ ∃k : set, nat_p k ∧ m = ordsucc k.
An exact proof term for the current goal is (nat_inv m HmNat).
We prove the intermediate claim Hexk: ∃k : set, nat_p k ∧ m = ordsucc k.
Apply (Hmcase (∃k : set, nat_p k ∧ m = ordsucc k)) to the current goal.
Assume Hm0: m = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hmne0 Hm0).
Assume H.
An exact proof term for the current goal is H.
Apply Hexk to the current goal.
Let k be given.
Assume Hkconj.
We prove the intermediate claim Hkeq: m = ordsucc k.
An exact proof term for the current goal is (andER (nat_p k) (m = ordsucc k) Hkconj).
We prove the intermediate claim HkNat: nat_p k.
An exact proof term for the current goal is (andEL (nat_p k) (m = ordsucc k) Hkconj).
We prove the intermediate claim HkOrd: ordinal k.
An exact proof term for the current goal is (nat_p_ordinal k HkNat).
We prove the intermediate claim H0ltm: 0 < m.
rewrite the current goal using Hkeq (from left to right).
An exact proof term for the current goal is (ordinal_ordsucc_pos k HkOrd).
We prove the intermediate claim HVdef: V = {y ∈ R|Rlt b y}.
Use reflexivity.
We prove the intermediate claim HxVsep: x ∈ {y ∈ R|Rlt b y}.
rewrite the current goal using HVdef (from right to left).
An exact proof term for the current goal is HxV.
We prove the intermediate claim HmVsep: inv_nat m ∈ {y ∈ R|Rlt b y}.
rewrite the current goal using Hxeq (from right to left).
An exact proof term for the current goal is HxVsep.
We prove the intermediate claim HbInvRlt: Rlt b (inv_nat m).
An exact proof term for the current goal is (SepE2 R (λy0 : set ⇒ Rlt b y0) (inv_nat m) HmVsep).
We prove the intermediate claim HbInvLt: b < inv_nat m.
An exact proof term for the current goal is (RltE_lt b (inv_nat m) HbInvRlt).
We prove the intermediate claim HinvS: SNo (inv_nat m).
An exact proof term for the current goal is (SNo_recip_SNo m HmS).
We prove the intermediate claim HmbLt: mul_SNo m b < mul_SNo m (inv_nat m).
An exact proof term for the current goal is (pos_mul_SNo_Lt m b (inv_nat m) HmS H0ltm HbS HinvS HbInvLt).
We prove the intermediate claim HmbLt1: mul_SNo m b < 1.
We prove the intermediate claim Hminv: mul_SNo m (inv_nat m) = 1.
An exact proof term for the current goal is (recip_SNo_invR m HmS Hmne0).
rewrite the current goal using Hminv (from right to left).
An exact proof term for the current goal is HmbLt.
We prove the intermediate claim HmLtrdiv: m < div_SNo 1 b.
An exact proof term for the current goal is (div_SNo_pos_LtR 1 b m SNo_1 HbS HmS H0ltb HmbLt1).
We prove the intermediate claim Hrdiv: div_SNo 1 b = r.
We prove the intermediate claim Hdivdef: div_SNo 1 b = mul_SNo 1 (recip_SNo b).
Use reflexivity.
rewrite the current goal using Hdivdef (from left to right).
rewrite the current goal using (mul_SNo_oneL (recip_SNo b) (SNo_recip_SNo b HbS)) (from left to right).
Use reflexivity.
We prove the intermediate claim HmLtr: m < r.
rewrite the current goal using Hrdiv (from right to left).
An exact proof term for the current goal is HmLtrdiv.
We prove the intermediate claim HmLtN: m < N.
An exact proof term for the current goal is (SNoLt_tra m r N HmS HrS HNS HmLtr HrltN).
We prove the intermediate claim HmInN: m ∈ N.
An exact proof term for the current goal is (ordinal_SNoLt_In m N HmOrd HNOrd HmLtN).
We prove the intermediate claim HmInI: m ∈ I.
Apply setminusI to the current goal.
An exact proof term for the current goal is HmInN.
An exact proof term for the current goal is Hmnot0.
An exact proof term for the current goal is (ReplI I (λt : set ⇒ inv_nat t) m HmInI).
An exact proof term for the current goal is (Subq_finite Big HBigFin (K_set ∩ V) Hsub).
∎