Let i and j be given.
Assume HiO: i ∈ ω.
Assume HjO: j ∈ ω.
Assume Hij: i ∈ j.
Set mi to be the term ordsucc i.
Set mj to be the term ordsucc j.
We prove the intermediate claim HiOrd: ordinal i.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal i HiO).
We prove the intermediate claim HjOrd: ordinal j.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal j HjO).
We prove the intermediate claim Hijlt: i < j.
An exact proof term for the current goal is (ordinal_In_SNoLt j HjOrd i Hij).
We prove the intermediate claim HiS: SNo i.
An exact proof term for the current goal is (omega_SNo i HiO).
We prove the intermediate claim HjS: SNo j.
An exact proof term for the current goal is (omega_SNo j HjO).
We prove the intermediate claim HmiS: SNo mi.
An exact proof term for the current goal is (omega_SNo mi (omega_ordsucc i HiO)).
We prove the intermediate claim HmjS: SNo mj.
An exact proof term for the current goal is (omega_SNo mj (omega_ordsucc j HjO)).
We prove the intermediate claim Hsucclt: mi < mj.
We will prove mi < mj.
rewrite the current goal using (add_SNo_1_ordsucc i HiO) (from right to left).
rewrite the current goal using (add_SNo_1_ordsucc j HjO) (from right to left).
An exact proof term for the current goal is (add_SNo_Lt1 i 1 j HiS SNo_1 HjS Hijlt).
We prove the intermediate claim HmiNot0: mi ≠ 0.
An exact proof term for the current goal is (neq_ordsucc_0 i).
We prove the intermediate claim HmjNot0: mj ≠ 0.
An exact proof term for the current goal is (neq_ordsucc_0 j).
We prove the intermediate claim HinvmiR: inv_nat mi ∈ R.
An exact proof term for the current goal is (inv_nat_real mi (omega_ordsucc i HiO)).
We prove the intermediate claim HinvmiS: SNo (inv_nat mi).
An exact proof term for the current goal is (real_SNo (inv_nat mi) HinvmiR).
We prove the intermediate claim HmiNotIn0: mi ∉ {0}.
Assume Hmi0: mi ∈ {0}.
We prove the intermediate claim Heq0: mi = 0.
An exact proof term for the current goal is (SingE 0 mi Hmi0).
An exact proof term for the current goal is (HmiNot0 Heq0).
We prove the intermediate claim HmiIn: mi ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} mi (omega_ordsucc i HiO) HmiNotIn0).
We prove the intermediate claim HinvmiPosR: Rlt 0 (inv_nat mi).
An exact proof term for the current goal is (inv_nat_pos mi HmiIn).
We prove the intermediate claim HinvmiPos: 0 < inv_nat mi.
An exact proof term for the current goal is (RltE_lt 0 (inv_nat mi) HinvmiPosR).
We prove the intermediate claim HmulLt: mul_SNo (inv_nat mi) mi < mul_SNo (inv_nat mi) mj.
An exact proof term for the current goal is (pos_mul_SNo_Lt (inv_nat mi) mi mj HinvmiS HinvmiPos HmiS HmjS Hsucclt).
We prove the intermediate claim HmulEq: mul_SNo (inv_nat mi) mi = 1.
We will prove mul_SNo (inv_nat mi) mi = 1.
rewrite the current goal using (mul_SNo_com (inv_nat mi) mi HinvmiS HmiS) (from left to right).
We prove the intermediate claim Hinvdef: inv_nat mi = recip_SNo mi.
Use reflexivity.
rewrite the current goal using Hinvdef (from left to right).
An exact proof term for the current goal is (recip_SNo_invR mi HmiS HmiNot0).
We prove the intermediate claim HoneLt: 1 < mul_SNo (inv_nat mi) mj.
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 Hmjpos: 0 < mj.
An exact proof term for the current goal is (ordinal_ordsucc_pos j HjOrd).
We prove the intermediate claim HdivLt: div_SNo 1 mj < inv_nat mi.
An exact proof term for the current goal is (div_SNo_pos_LtL 1 mj (inv_nat mi) SNo_1 HmjS HinvmiS Hmjpos HoneLt).
We prove the intermediate claim HdivEq: div_SNo 1 mj = inv_nat mj.
An exact proof term for the current goal is (div_SNo_1_eq_inv_nat mj HmjS).
We prove the intermediate claim HinvLtS: inv_nat mj < inv_nat mi.
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 HinvmiInR: inv_nat mi ∈ R.
An exact proof term for the current goal is HinvmiR.
We prove the intermediate claim HinvMjR: inv_nat mj ∈ R.
An exact proof term for the current goal is (inv_nat_real mj (omega_ordsucc j HjO)).
An exact proof term for the current goal is (RltI (inv_nat mj) (inv_nat mi) HinvMjR HinvmiInR HinvLtS).
∎