proposition: Lemma Qpairio_gle2P k n l m: natp k -> natp n -> natp l -> natp m -> let f:= fun k n => (k *c (\2c ^c n)) in gle Qpairi_o (Qpairi k n) (Qpairi l m) <-> (exists p, [/\ natp p, m = n +c p, (f k p) <=c l & (csucc l) <=c (f (csucc k) p)]).
proof: Proof. move=> kN nN lN mN f. have n2N: natp (\2c ^c n) by fprops. split; last first. move=> [p [pN eq le1 le2]]. apply /(Qpairio_gle1P kN nN lN mN); rewrite eq cpow_sum2; split. rewrite cprodA (cprodC k _) - cprodA cprodC. apply: cprod_Mlele; fprops. rewrite cprodA (cprodC (csucc k) _) - cprodA cprodC. apply: cprod_Mlele; fprops. move/ (Qpairio_gle1P kN nN lN mN). rewrite (cprodC (csucc l) _)(cprodC (csucc k) _). move=> [r1 r02]; move: (r02). have m2N: natp (\2c ^c m) by fprops. rewrite cprod_nS // cprod_nS //. rewrite (cprodC _ l)(cprodC _ k) -/(f k m) -/(f l n) => r2. have r3:(\2c ^c n) <=c (\2c ^c n) by fprops. move: (csum_Mlele r1 r3) => r4. move: (cleT r4 r2) => r5. have fN: natp (f k m) by rewrite /f; fprops. move: (csum_le2l fN n2N m2N r5) => aux. have nm: n <=c m. case: (cleT_el (CS_nat nN) (CS_nat mN)) => // nm. case: (cleNgt aux (cpow_Meqlt NS2 nN nm clt_12)). move: (cdiff_pr nm); set p := (m -c n) => cp. have pN: natp p by apply: NS_diff. move: r1 r02; rewrite - cp cpow_sum2. set ptn:= (\2c ^c n). rewrite cprodA (cprodC k _) - cprodA -/(f k p)(cprodC _ ptn). rewrite - cprodA (cprodC _ (csucc k)) -/(f (csucc k) p) => r1 r6. have knz: ptn <> \0c by apply: cpow2_nz. have fkpN: natp (f k p) by rewrite /f; fprops. have fkspN: natp (f (csucc k) p) by rewrite /f; fprops. exists p; split => //. apply: (cprod_le2l n2N fkpN lN knz r1). apply: (cprod_le2l n2N (NS_succ lN) fkspN knz r6). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)