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 HmiO: mi ∈ ω.
An exact proof term for the current goal is (omega_ordsucc i HiO).
We prove the intermediate claim HmjO: mj ∈ ω.
An exact proof term for the current goal is (omega_ordsucc j HjO).
We prove the intermediate claim HinvMiR: inv_nat mi ∈ R.
An exact proof term for the current goal is (inv_nat_real mi HmiO).
We prove the intermediate claim HinvMjR: inv_nat mj ∈ R.
An exact proof term for the current goal is (inv_nat_real mj HmjO).
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 HinvMjS: SNo (inv_nat mj).
An exact proof term for the current goal is (real_SNo (inv_nat mj) HinvMjR).
We prove the intermediate claim HinvLt: Rlt (inv_nat mj) (inv_nat mi).
An exact proof term for the current goal is (inv_nat_ordsucc_antitone_local2 i j HiO HjO Hij).
We prove the intermediate claim HinvLtS: inv_nat mj < inv_nat mi.
An exact proof term for the current goal is (RltE_lt (inv_nat mj) (inv_nat mi) HinvLt).
We prove the intermediate claim HnegLtS: minus_SNo (inv_nat mi) < minus_SNo (inv_nat mj).
An exact proof term for the current goal is (minus_SNo_Lt_contra (inv_nat mj) (inv_nat mi) HinvMjS HinvMiS HinvLtS).
We prove the intermediate claim HxLtS: add_SNo 1 (minus_SNo (inv_nat mi)) < add_SNo 1 (minus_SNo (inv_nat mj)).
An exact proof term for the current goal is (add_SNo_Lt2 1 (minus_SNo (inv_nat mi)) (minus_SNo (inv_nat mj)) SNo_1 (SNo_minus_SNo (inv_nat mi) HinvMiS) (SNo_minus_SNo (inv_nat mj) HinvMjS) HnegLtS).
We prove the intermediate claim HxR: add_SNo 1 (minus_SNo (inv_nat mi)) ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo (inv_nat mi)) (real_minus_SNo (inv_nat mi) HinvMiR)).
We prove the intermediate claim HyR: add_SNo 1 (minus_SNo (inv_nat mj)) ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo (inv_nat mj)) (real_minus_SNo (inv_nat mj) HinvMjR)).
We prove the intermediate claim HxLtR: Rlt (add_SNo 1 (minus_SNo (inv_nat mi))) (add_SNo 1 (minus_SNo (inv_nat mj))).
An exact proof term for the current goal is (RltI (add_SNo 1 (minus_SNo (inv_nat mi))) (add_SNo 1 (minus_SNo (inv_nat mj))) HxR HyR HxLtS).
Apply (order_rel_setprod_R_R_intro (add_SNo 1 (minus_SNo (inv_nat mi))) (eps_ 1) (add_SNo 1 (minus_SNo (inv_nat mj))) (eps_ 1)) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is HxLtR.
∎