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 HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
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.
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).
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: 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 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 HkOrd: ordinal k.
An exact proof term for the current goal is (nat_p_ordinal k HkNat).
We prove the intermediate claim Hpos: 0 < n.
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 HSn: SNo n.
An exact proof term for the current goal is (omega_SNo n HnO).
We prove the intermediate claim Hposcase: inv_nat n = recip_SNo_pos n.
An exact proof term for the current goal is (recip_SNo_poscase n Hpos).
We prove the intermediate claim HrecipPos: 0 < recip_SNo_pos n.
An exact proof term for the current goal is (recip_SNo_pos_is_pos n HSn Hpos).
We prove the intermediate claim HinvPos: 0 < inv_nat n.
rewrite the current goal using Hposcase (from left to right).
An exact proof term for the current goal is HrecipPos.
We prove the intermediate claim HinvR: inv_nat n ∈ R.
An exact proof term for the current goal is (inv_nat_real n HnO).
An exact proof term for the current goal is (RltI 0 (inv_nat n) real_0 HinvR HinvPos).
∎