Let α, β, 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 (α ∩ β).
An exact proof term for the current goal is ordinal_binintersect α β Ha Hb.
Apply PNoLt_trichotomy_or_ p q (α ∩ β) Lab to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: PNoLt_ (α ∩ β) 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_ (α ∩ β) p q.
Apply ordinal_trichotomy_or α β Ha Hb to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: α ∈ β.
We prove the intermediate claim L1: α ∩ β = α.
An exact proof term for the current goal is binintersect_Subq_eq_1 α β (Hb1 α H2).
We prove the intermediate claim L2: PNoEq_ α 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 α) to the current goal.
Assume H3: q α.
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_ α 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 α.
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_ α 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: α = β.
We prove the intermediate claim L1: α ∩ β = α.
rewrite the current goal using H2 (from right to left).
An exact proof term for the current goal is binintersect_Subq_eq_1 α α (Subq_ref α).
We prove the intermediate claim L2: PNoEq_ α 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_ α p q.
An exact proof term for the current goal is L2.
Assume H2: β ∈ α.
We prove the intermediate claim L1: α ∩ β = β.
rewrite the current goal using binintersect_com (from left to right).
An exact proof term for the current goal is binintersect_Subq_eq_1 β α (Ha1 β H2).
We prove the intermediate claim L2: PNoEq_ β 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 β) to the current goal.
Assume H3: p β.
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_ β 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 β.
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_ β 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_ (α ∩ β) 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.
∎