proposition: Lemma Qpairio_gle4 x y: inc x (substrate Qpairi_o) -> inc y (substrate Qpairi_o) -> [\/ gle Qpairi_o x y, gle Qpairi_o y x | (forall z : Set, gle Qpairi_o x z -> gle Qpairi_o y z -> False)].
proof: Proof. move=> xs ys. case: (p_or_not_p (gle Qpairi_o x y)) => h1; first by constructor 1. case: (p_or_not_p (gle Qpairi_o y x)) => h2; first by constructor 2. move: (xs) (ys); rewrite (proj2 Qpairio_osr) => /Qpairis_prP. move=> [k [n [kN nN xv]]] /Qpairis_prP [l [m [lN mN yv]]]. constructor 3; rewrite xv yv; move=> z le1 le2. case: (cleT_ee (CS_nat nN) (CS_nat mN)) => // nm. case: h1; rewrite xv yv; apply: (Qpairio_gle3 kN nN lN mN nm le1 le2). case: h2; rewrite xv yv; apply: (Qpairio_gle3 lN mN kN nN nm le2 le1). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)