Let alpha, beta, p and q be given.
Assume Ha Hb.
Apply Ha to the current goal.
Assume Ha1 _.
Apply Hb to the current goal.
Assume Hb1 _.
We prove the intermediate claim Lab: ordinal (alpha ∩ beta).
An exact proof term for the current goal is ordinal_binintersect alpha beta Ha Hb.
Apply PNoLt_trichotomy_or_ p q (alpha ∩ beta) Lab to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: PNoLt_ (alpha ∩ beta) p q.
Apply or3I1 to the current goal.
Apply PNoLtI1 to the current goal.
An exact proof term for the current goal is H1.
Assume H1: PNoEq_ (alpha ∩ beta) p q.
Apply ordinal_trichotomy_or alpha beta Ha Hb to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: alpha ∈ beta.
We prove the intermediate claim L1: alpha ∩ beta = alpha.
An exact proof term for the current goal is binintersect_Subq_eq_1 alpha beta (Hb1 alpha H2).
We prove the intermediate claim L2: PNoEq_ alpha p q.
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is H1.
Apply xm (q alpha) to the current goal.
Assume H3: q alpha.
Apply or3I1 to the current goal.
Apply PNoLtI2 to the current goal.
An exact proof term for the current goal is H2.
We will prove PNoEq_ alpha p q.
An exact proof term for the current goal is L2.
An exact proof term for the current goal is H3.
Assume H3: ¬ q alpha.
Apply or3I3 to the current goal.
Apply PNoLtI3 to the current goal.
An exact proof term for the current goal is H2.
We will prove PNoEq_ alpha q p.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is L2.
An exact proof term for the current goal is H3.
Assume H2: alpha = beta.
We prove the intermediate claim L1: alpha ∩ beta = alpha.
rewrite the current goal using H2 (from right to left).
An exact proof term for the current goal is binintersect_Subq_eq_1 alpha alpha (Subq_ref alpha).
We prove the intermediate claim L2: PNoEq_ alpha p q.
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is H1.
Apply or3I2 to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is H2.
We will prove PNoEq_ alpha p q.
An exact proof term for the current goal is L2.
Assume H2: beta ∈ alpha.
We prove the intermediate claim L1: alpha ∩ beta = beta.
rewrite the current goal using binintersect_com (from left to right).
An exact proof term for the current goal is binintersect_Subq_eq_1 beta alpha (Ha1 beta H2).
We prove the intermediate claim L2: PNoEq_ beta p q.
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is H1.
Apply xm (p beta) to the current goal.
Assume H3: p beta.
Apply or3I3 to the current goal.
Apply PNoLtI2 to the current goal.
An exact proof term for the current goal is H2.
We will prove PNoEq_ beta q p.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is L2.
An exact proof term for the current goal is H3.
Assume H3: ¬ p beta.
Apply or3I1 to the current goal.
Apply PNoLtI3 to the current goal.
An exact proof term for the current goal is H2.
We will prove PNoEq_ beta p q.
An exact proof term for the current goal is L2.
An exact proof term for the current goal is H3.
Assume H1: PNoLt_ (alpha ∩ beta) q p.
Apply or3I3 to the current goal.
Apply PNoLtI1 to the current goal.
rewrite the current goal using binintersect_com (from left to right).
An exact proof term for the current goal is H1.
∎