proposition: Lemma ordering_pair1 x: ordinal_pair x -> ((P x <=o Q x) /\ ord_pair_max x = Q x) \/ ((Q x <=o P x) /\ ord_pair_max x = P x).
proof: Proof. move=> [px op oq]; case:(oleT_ee op oq)=> h ; [left | right ]; split => //. by apply: omax_xy. by apply: omax_yx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)