proposition: Lemma Qpairio_gle1P 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) <-> ((f k m) <=c (f l n) /\ (f (csucc l) n) <=c (f (csucc k) m)).
proof: Proof. move=> kN nN lN mN f. move: (Qpairis_pr2 lN mN) => [p4 p5]. split. move /Qpairio_gleP => [p1 p2 p3]. move: (p3 _ p4) => /Qpairis_pr1P [q1 q2]. move: (p3 _ p5) => /Qpairis_pr1P [q3 q4]. split. by apply /(Qpair_le0P kN nN lN mN). by apply /(Qpair_le0P (NS_succ lN) mN (NS_succ kN) nN). move => [] /(Qpair_le0P kN nN lN mN) pa /(Qpair_le0P (NS_succ lN) mN (NS_succ kN) nN) pb. apply /Qpairio_gleP;split => //. by apply /Qpairis_prP;exists k, n. by apply /Qpairis_prP;exists l, m. move=> t /Qpairis_pr1P [q3 q4]; move:(qleT pa q3) (qleT q4 pb) => r1 r2. apply /Qpairis_pr1P;split => //. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)