proposition: Lemma Qpair_le0P a b c d: natp a -> natp b -> natp c -> natp d -> let f:= fun k n => k *c (\2c ^c n) in (Qpair a b) <=q (Qpair c d) <-> (f a d) <=c (f c b).
proof: Proof. move => aN bN cN dN /=. apply: (iff_trans (BQ_le_pair (BZ_of_nat_i aN) (zpow2_pos bN)(BZ_of_nat_i cN) (zpow2_pos dN))). move: (NS_pow NS2 dN) (NS_pow NS2 bN) => p1N p2N. rewrite (BZprod_cN aN p1N) (BZprod_cN p2N cN) (cprodC c). apply:iff_sym. apply: (zle_cN (NS_prod aN p1N) (NS_prod p2N cN)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)