proposition: Lemma Qpairio_gle3 k n l m z: natp k -> natp n -> natp l -> natp m -> n <=c m -> gle Qpairi_o (Qpairi k n) z -> gle Qpairi_o(Qpairi l m) z -> gle Qpairi_o (Qpairi k n) (Qpairi l m).
proof: Proof. move=> kN nN lN mN nm le1 le2. have: inc z (substrate Qpairi_o) by order_tac. rewrite (proj2 Qpairio_osr) => / Qpairis_prP [i [s [iN sN zv]]]. move: le1 le2; rewrite zv => /(Qpairio_gle2P kN nN iN sN) [p [pN s1 le1 le2]] /(Qpairio_gle2P lN mN iN sN) [q [qN s2 le3 le4]]. move: (cdiff_pr nm); set t:=(m -c n) => tp. have tN: natp t by apply: NS_diff. have ptq: p = q +c t. apply: (@csum_eq2l n) => //; fprops. by rewrite (csumC q t) csumA tp - s1. have ptq1: p = t +c q by rewrite csumC. move: le1 le2; rewrite ptq1 cpow_sum2 cprodA cprodA => le1 le2. apply /(Qpairio_gle2P kN nN lN mN); exists t. move: le1 le2 le3 le4. set kt := (k *c (\2c ^c t)). set kpt := ((csucc k) *c (\2c ^c t)). set q2:= (\2c ^c q). move: NS2 => bs2. have kpN: natp kt by rewrite /kt; fprops. have kptN: natp kpt by rewrite /kpt; fprops. have q2N: natp q2 by rewrite / q2; fprops. have kptqN: natp (kpt *c q2) by fprops. have lpqN: natp ((csucc l) *c q2) by fprops. move => le1 /(cleSltP iN) le2 le3 /(cleSltP iN) le4. move: (cle_ltT le1 le4) (cle_ltT le3 le2). have knz: q2 <> \0c. by apply: cpow_nz; fprops. rewrite !(cprodC _ q2) => le5 le6;split => //. apply /cltSleP=>//;apply: (@cprod_lt2l q2) => //; fprops. apply /(cleSltP lN). apply: (@cprod_lt2l q2) => //. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)