Let r be given.
Assume HrR: r ∈ R.
Assume HrposR: Rlt 0 r.
Set rinv to be the term recip_SNo r.
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
We prove the intermediate claim Hrpos: 0 < r.
An exact proof term for the current goal is (RltE_lt 0 r HrposR).
We prove the intermediate claim HrinvR: rinv ∈ R.
An exact proof term for the current goal is (real_recip_SNo r HrR).
We prove the intermediate claim HrinvS: SNo rinv.
An exact proof term for the current goal is (real_SNo rinv HrinvR).
We prove the intermediate claim HrinvPos: 0 < rinv.
An exact proof term for the current goal is (recip_SNo_of_pos_is_pos r HrS Hrpos).
We prove the intermediate claim HrinvNN: 0 ≤ rinv.
An exact proof term for the current goal is (SNoLtLe 0 rinv HrinvPos).
We prove the intermediate claim Hexn: ∃n ∈ ω, n ≤ rinv ∧ rinv < ordsucc n.
An exact proof term for the current goal is (nonneg_real_nat_interval rinv HrinvR HrinvNN).
Apply Hexn to the current goal.
Let n be given.
Assume Hnconj.
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (andEL (n ∈ ω) (n ≤ rinv ∧ rinv < ordsucc n) Hnconj).
We prove the intermediate claim Hnrest: n ≤ rinv ∧ rinv < ordsucc n.
An exact proof term for the current goal is (andER (n ∈ ω) (n ≤ rinv ∧ rinv < ordsucc n) Hnconj).
We prove the intermediate claim HrinvLt: rinv < ordsucc n.
An exact proof term for the current goal is (andER (n ≤ rinv) (rinv < ordsucc n) Hnrest).
We prove the intermediate claim HnOrd: ordinal n.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal n HnO).
We prove the intermediate claim HNpos: 0 < ordsucc n.
An exact proof term for the current goal is (ordinal_ordsucc_pos n HnOrd).
We prove the intermediate claim HNinO: ordsucc n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n HnO).
We prove the intermediate claim HNS: SNo (ordsucc n).
An exact proof term for the current goal is (omega_SNo (ordsucc n) HNinO).
We prove the intermediate claim HmulLt: mul_SNo r rinv < mul_SNo r (ordsucc n).
An exact proof term for the current goal is (pos_mul_SNo_Lt r rinv (ordsucc n) HrS Hrpos HrinvS HNS HrinvLt).
We prove the intermediate claim Hrne0: r ≠ 0.
An exact proof term for the current goal is (SNo_pos_ne0 r HrS Hrpos).
We prove the intermediate claim HmulEq: mul_SNo r rinv = 1.
We will prove mul_SNo r rinv = 1.
We prove the intermediate claim Hrinvdef: rinv = recip_SNo r.
Use reflexivity.
rewrite the current goal using Hrinvdef (from left to right).
An exact proof term for the current goal is (recip_SNo_invR r HrS Hrne0).
We prove the intermediate claim HoneLt: 1 < mul_SNo r (ordsucc n).
rewrite the current goal using HmulEq (from right to left) at position 1.
An exact proof term for the current goal is HmulLt.
We prove the intermediate claim HdivLt: div_SNo 1 (ordsucc n) < r.
An exact proof term for the current goal is (div_SNo_pos_LtL 1 (ordsucc n) r SNo_1 HNS HrS HNpos HoneLt).
We prove the intermediate claim HdivEq: div_SNo 1 (ordsucc n) = inv_nat (ordsucc n).
An exact proof term for the current goal is (div_SNo_1_eq_inv_nat (ordsucc n) HNS).
We prove the intermediate claim HinvLtS: inv_nat (ordsucc n) < r.
rewrite the current goal using HdivEq (from right to left).
An exact proof term for the current goal is HdivLt.
We prove the intermediate claim HinvR: inv_nat (ordsucc n) ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc n) HNinO).
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HnO.
An exact proof term for the current goal is (RltI (inv_nat (ordsucc n)) r HinvR HrR HinvLtS).
∎