Let a and b be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Assume Hnot0a: ¬ (Rlt 0 a).
Assume H0b: Rlt 0 b.
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 H0b).
We prove the intermediate claim Hbne0: b ≠ 0.
Assume Hb0: b = 0.
We prove the intermediate claim H00: 0 < 0.
rewrite the current goal using Hb0 (from right to left) at position 2.
An exact proof term for the current goal is H0ltb.
An exact proof term for the current goal is ((SNoLt_irref 0) H00).
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: n ∈ ω ∧ (n ≤ r ∧ r < ordsucc n).
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 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 H0ltN: 0 < N.
An exact proof term for the current goal is (ordinal_ordsucc_pos n HnOrd).
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 Hineq: mul_SNo b r < mul_SNo b N.
An exact proof term for the current goal is (pos_mul_SNo_Lt b r N HbS H0ltb HrS HNS HrltN).
We prove the intermediate claim Hbr1: mul_SNo b r = 1.
An exact proof term for the current goal is (recip_SNo_invR b HbS Hbne0).
We prove the intermediate claim H1ltbN: 1 < mul_SNo b N.
rewrite the current goal using Hbr1 (from right to left).
An exact proof term for the current goal is Hineq.
We prove the intermediate claim HinvLt: div_SNo 1 N < b.
An exact proof term for the current goal is (div_SNo_pos_LtL 1 N b SNo_1 HNS (real_SNo b HbR) H0ltN H1ltbN).
We prove the intermediate claim HinvEq: div_SNo 1 N = inv_nat N.
We will prove div_SNo 1 N = inv_nat N.
We prove the intermediate claim Hdivdef: div_SNo 1 N = mul_SNo 1 (recip_SNo N).
Use reflexivity.
We prove the intermediate claim Hinvdef: inv_nat N = recip_SNo N.
Use reflexivity.
rewrite the current goal using Hdivdef (from left to right).
rewrite the current goal using Hinvdef (from left to right) at position 2.
rewrite the current goal using (mul_SNo_oneL (recip_SNo N) (SNo_recip_SNo N HNS)) (from left to right).
Use reflexivity.
We prove the intermediate claim Hyltb: inv_nat N < b.
rewrite the current goal using HinvEq (from right to left).
An exact proof term for the current goal is HinvLt.
We prove the intermediate claim HyR: inv_nat N ∈ R.
An exact proof term for the current goal is (inv_nat_real N HNOmega).
We prove the intermediate claim HyRltb: Rlt (inv_nat N) b.
An exact proof term for the current goal is (RltI (inv_nat N) b HyR HbR Hyltb).
We prove the intermediate claim HNnot0: N ∉ {0}.
Assume HNin: N ∈ {0}.
We prove the intermediate claim HNeq0: N = 0.
An exact proof term for the current goal is (SingE 0 N HNin).
We prove the intermediate claim H00: 0 < 0.
rewrite the current goal using HNeq0 (from right to left) at position 2.
An exact proof term for the current goal is H0ltN.
An exact proof term for the current goal is ((SNoLt_irref 0) H00).
We prove the intermediate claim HNinSetminus: N ∈ ω ∖ {0}.
Apply setminusI to the current goal.
An exact proof term for the current goal is HNOmega.
An exact proof term for the current goal is HNnot0.
We prove the intermediate claim HyK: inv_nat N ∈ K_set.
An exact proof term for the current goal is (ReplI (ω ∖ {0}) (λm : set ⇒ inv_nat m) N HNinSetminus).
We prove the intermediate claim Hypos: Rlt 0 (inv_nat N).
An exact proof term for the current goal is (inv_nat_pos N HNinSetminus).
We prove the intermediate claim HnotHyLta: ¬ (Rlt (inv_nat N) a).
Assume Hylta: Rlt (inv_nat N) a.
We prove the intermediate claim H0lta: Rlt 0 a.
An exact proof term for the current goal is (Rlt_tra 0 (inv_nat N) a Hypos Hylta).
An exact proof term for the current goal is (Hnot0a H0lta).
We use (inv_nat N) to witness the existential quantifier.
Apply andI to the current goal.
We will prove inv_nat N ∈ halfopen_interval_left a b.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ¬ (Rlt x0 a) ∧ Rlt x0 b) (inv_nat N) HyR (andI (¬ (Rlt (inv_nat N) a)) (Rlt (inv_nat N) b) HnotHyLta HyRltb)).
An exact proof term for the current goal is HyK.
∎