proposition: Lemma Exercise1_24b x: inc x (substrate Qpairi_o) -> ~ (maximal Qpairi_o x).
proof: Proof. rewrite (proj2 Qpairio_osr) => /Qpairis_prP [k [n [kN nN xv]]]. set y := Qpairi (k *c \2c) (csucc n). move: NS2 NS1 => b2 b1. have aux: gle Qpairi_o x y. have p1: natp (k *c \2c) by fprops. have p2: natp (csucc n) by fprops. have p3: cardinalp k by fprops. have p4: cardinalp \2c by fprops. have p5: cardinalp (k *c \2c) by fprops. rewrite xv /y; apply /Qpairio_gle2P => //. exists \1c. rewrite (cpowx1 p4) - csucc_pr4 //; fprops; split;fprops. rewrite !csucc_pr4 // cprodDl. have ->: \1c *c \2c = \1c +c \1c by rewrite cprod1l// csum_11. rewrite csumA. apply: Nsum_M0le; fprops. move=> [_ h]; move: (h _ aux). have k2N: natp (k *c \2c) by fprops. rewrite xv /y=> xy. move: (Qpairio_eq k2N (NS_succ nN) kN nN xy) => [_ sn]. by move: nN => /NatP /finite_cP [_] []. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)