Let n and m be given.
Assume HnO: n ∈ ω.
Assume HmO: m ∈ ω.
Assume Heq: equip n m.
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 HmNat: nat_p m.
An exact proof term for the current goal is (omega_nat_p m HmO).
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 HmOrd: ordinal m.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal m HmO).
We prove the intermediate claim HnmAt: atleastp n m.
An exact proof term for the current goal is (equip_atleastp n m Heq).
We prove the intermediate claim HmnAt: atleastp m n.
We prove the intermediate claim HeqSym: equip m n.
An exact proof term for the current goal is (equip_sym n m Heq).
An exact proof term for the current goal is (equip_atleastp m n HeqSym).
We prove the intermediate claim Hcase: n ∈ m ∨ m ⊆ n.
An exact proof term for the current goal is (ordinal_In_Or_Subq n m HnOrd HmOrd).
Apply (Hcase (n = m)) to the current goal.
Assume HnIn: n ∈ m.
Apply FalseE to the current goal.
We prove the intermediate claim HsuccSub: ordsucc n ⊆ m.
An exact proof term for the current goal is (ordinal_ordsucc_In_Subq m HmOrd n HnIn).
We prove the intermediate claim HsuccAtm: atleastp (ordsucc n) m.
An exact proof term for the current goal is (Subq_atleastp (ordsucc n) m HsuccSub).
We prove the intermediate claim HsuccAtn: atleastp (ordsucc n) n.
An exact proof term for the current goal is (atleastp_tra (ordsucc n) m n HsuccAtm HmnAt).
An exact proof term for the current goal is (Pigeonhole_not_atleastp_ordsucc n HnNat HsuccAtn).
Assume HmSub: m ⊆ n.
We prove the intermediate claim Hcase2: m ∈ n ∨ n ⊆ m.
An exact proof term for the current goal is (ordinal_In_Or_Subq m n HmOrd HnOrd).
We prove the intermediate claim HnSub: n ⊆ m.
Apply (Hcase2 (n ⊆ m)) to the current goal.
Assume HmIn: m ∈ n.
Apply FalseE to the current goal.
We prove the intermediate claim HsuccSub: ordsucc m ⊆ n.
An exact proof term for the current goal is (ordinal_ordsucc_In_Subq n HnOrd m HmIn).
We prove the intermediate claim HsuccAtn: atleastp (ordsucc m) n.
An exact proof term for the current goal is (Subq_atleastp (ordsucc m) n HsuccSub).
We prove the intermediate claim HsuccAtm: atleastp (ordsucc m) m.
An exact proof term for the current goal is (atleastp_tra (ordsucc m) n m HsuccAtn HnmAt).
An exact proof term for the current goal is (Pigeonhole_not_atleastp_ordsucc m HmNat HsuccAtm).
Assume HnSubm: n ⊆ m.
An exact proof term for the current goal is HnSubm.
Apply set_ext to the current goal.
An exact proof term for the current goal is HnSub.
An exact proof term for the current goal is HmSub.
∎