proposition: Lemma Exercise1_24c: anti_directed Qpairi_o.
proof: Proof. move: Qpairio_osr => [h0 sr]. apply/(Exercise1_23hP h0); split => //. move=> x y [lexy nxy]. have xs: inc x (substrate Qpairi_o) by order_tac. have ys: inc y (substrate Qpairi_o) by order_tac. move: (xs) (ys); rewrite sr => /Qpairis_prP [k [n [kN nN xv]]] /Qpairis_prP [l [m [lN mN yv]]]. move: lexy; rewrite xv yv=> /(Qpairio_gle2P kN nN lN mN) [p [pN nm le1 le2]]. have skN:= NS_succ kN. case: (equal_or_not p \0c) => pz. move: le1 le2; rewrite pz cpowx0 !cprod1r; fprops => le1. move /(cleSSP (CS_nat lN) (CS_nat kN)) => le2. by case: nxy; rewrite xv yv (cleA le1 le2) nm pz Nsum0r. have nmn: m <> n. dneg mn. apply: (@csum_eq2l n) => //; fprops. by rewrite -nm mn Nsum0r. set q2:= (\2c ^c p) in le1 le2. set kq2 := (k *c q2) in le1. set l':= Yo (l = kq2) (csucc l) kq2. have l'N: natp l' by move: NS2=> b2; rewrite /l'/kq2/ q2; Ytac aux; fprops. have ll': l <> l'. rewrite /l'; Ytac aux =>//; exact: (proj2(cltS lN)). set z := Qpairi l' m. exists z => //. split; last first. rewrite /z => eq; move: (Qpairio_eq kN nN l'N mN eq) => [_ nm']. by case: nmn. apply /Qpairio_gle2P => //; exists p; rewrite -/ q2 -/kq2. have lsl: l <=c (csucc l) by apply: cleS. have p1:= cleT le1 lsl. have p2:= cleR (proj31 p1). have q2N: natp q2 by rewrite / q2; fprops. have kq2N: natp kq2 by rewrite /kq2; fprops. have skq2: natp ((csucc k) *c q2) by fprops. have knz: q2 <> \0c by apply: cpow2_nz. have le3: (csucc kq2) <=c ((csucc k) *c q2). apply /cleSltP => //; split; first exact : (cleT p1 le2). rewrite cprodC cprod_nS // cprodC -/kq2. dneg aux1; apply: (@csum_eq2l kq2) => //; fprops. by rewrite -aux1 Nsum0r. split => //; first by rewrite /l'; Ytac aux => //. rewrite /l'; Ytac aux => //. have slN: natp (csucc l) by fprops. have ckq2: cardinalp kq2 by fprops. apply /(cleSltP slN) => //; split => //. rewrite aux csucc_pr4// cprodC cprod_nS // cprodC -/kq2. move=> aux2. move: (csum_eq2l kq2N NS1 q2N aux2) => q21. move: NS1 (cpow_Mle1 CS2 pz) => oN. by rewrite -/ q2 - q21 - succ_one;move /(cleSltP oN) => [_ ];case. move=> t; rewrite /z=> le1a le2a. have mm: m <=c m by fprops. move: (Qpairio_gle3 lN mN l'N mN mm le1a le2a). move /(Qpairio_gle1P lN mN l'N mN). set m2:= (\2c ^c m). have m2N: natp m2 by rewrite /m2; fprops. have knz: m2 <> \0c by apply: cpow2_nz. rewrite !(cprodC _ m2); move => [le3 le4]. have le5: l <=c l'. apply: (@cprod_le2l m2) => //. have : (csucc l') <=c (csucc l). apply: (@cprod_le2l m2) => //; fprops. have cl: cardinalp l' by fprops. by move /(cleSSP cl (CS_nat lN)) => le6;case: ll'; apply:cleA. move=> x y xs ys. case: ( Qpairio_gle4 xs ys);first by constructor 1. by constructor 2. by move=> h; constructor 3; exists x => //; order_tac. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)