proposition: Lemma Qpair_eq k n m: natp k -> natp n -> natp m -> Qpair k n = Qpair (k *c \2c ^c m) (m +c n).
proof: Proof. move => kN nN mN. move: (NS_pow NS2 mN) => fN; move: (NS_prod kN fN) => pN. move: (zpow2_pos nN) (zpow2_pos (NS_sum mN nN)) => pa pb. apply/ (BQ_of_pair_prop5 (BZ_of_nat_i kN) pa (BZ_of_nat_i pN) pb). rewrite (BZprod_cN kN (NS_pow NS2 (NS_sum mN nN))). rewrite (BZprod_cN (NS_pow NS2 nN) pN); apply: f_equal. by rewrite (cprodC (\2c ^c n)) - cprodA - cpow_sum2. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)