Let n be given.
Assume HnIn: n ∈ ω ∖ {0}.
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (setminusE1 ω {0} n HnIn).
We prove the intermediate claim Hnnot0: n ∉ {0}.
An exact proof term for the current goal is (setminusE2 ω {0} n HnIn).
We prove the intermediate claim Hnneq0: n ≠ 0.
Assume Hn0: n = 0.
We prove the intermediate claim Hnin0: n ∈ {0}.
rewrite the current goal using Hn0 (from left to right).
An exact proof term for the current goal is (SingI 0).
An exact proof term for the current goal is (Hnnot0 Hnin0).
We prove the intermediate claim HinvR: inv_nat n ∈ R.
An exact proof term for the current goal is (inv_nat_real n HnO).
Apply (RleI (inv_nat n) 1 HinvR real_1) to the current goal.
We will prove ¬ (Rlt 1 (inv_nat n)).
Assume Hlt: Rlt 1 (inv_nat n).
We prove the intermediate claim HltS: 1 < inv_nat n.
An exact proof term for the current goal is (RltE_lt 1 (inv_nat n) Hlt).
We prove the intermediate claim HnS: SNo n.
An exact proof term for the current goal is (omega_SNo n HnO).
We prove the intermediate claim HinvS: SNo (inv_nat n).
An exact proof term for the current goal is (SNo_recip_SNo n HnS).
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
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 H1Ord: ordinal 1.
An exact proof term for the current goal is (nat_p_ordinal 1 nat_1).
We prove the intermediate claim HnCase: n = 0 ∨ ∃k : set, nat_p k ∧ n = ordsucc k.
An exact proof term for the current goal is (nat_inv n HnNat).
We prove the intermediate claim Hexk: ∃k : set, nat_p k ∧ n = ordsucc k.
Apply (HnCase (∃k : set, nat_p k ∧ n = ordsucc k)) to the current goal.
Assume Hn0: n = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnneq0 Hn0).
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 HkNat: nat_p k.
An exact proof term for the current goal is (andEL (nat_p k) (n = ordsucc k) Hkconj).
We prove the intermediate claim Hneq: n = ordsucc k.
An exact proof term for the current goal is (andER (nat_p k) (n = 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 H0ltn: 0 < n.
rewrite the current goal using Hneq (from left to right).
An exact proof term for the current goal is (ordinal_ordsucc_pos k HkOrd).
We prove the intermediate claim HmulLt: mul_SNo n 1 < mul_SNo n (inv_nat n).
An exact proof term for the current goal is (pos_mul_SNo_Lt n 1 (inv_nat n) HnS H0ltn SNo_1 HinvS HltS).
We prove the intermediate claim Hmul1: mul_SNo n 1 = n.
An exact proof term for the current goal is (mul_SNo_oneR n HnS).
We prove the intermediate claim HmulInv: mul_SNo n (inv_nat n) = 1.
An exact proof term for the current goal is (recip_SNo_invR n HnS Hnneq0).
We prove the intermediate claim Hnlt1: n < 1.
rewrite the current goal using Hmul1 (from right to left).
rewrite the current goal using HmulInv (from right to left) at position 2.
An exact proof term for the current goal is HmulLt.
We prove the intermediate claim HnIn1: n ∈ 1.
An exact proof term for the current goal is (ordinal_SNoLt_In n 1 HnOrd H1Ord Hnlt1).
We prove the intermediate claim Hcase1: n ∈ 0 ∨ n = 0.
An exact proof term for the current goal is (ordsuccE 0 n HnIn1).
We prove the intermediate claim Hn0: n = 0.
Apply (Hcase1 (n = 0)) to the current goal.
Assume HnIn0: n ∈ 0.
An exact proof term for the current goal is (EmptyE n HnIn0 (n = 0)).
Assume H.
An exact proof term for the current goal is H.
An exact proof term for the current goal is (Hnneq0 Hn0).
∎