proposition: Lemma zpow2_pos n: natp n -> inc (BZ_of_nat (\2c ^c n)) BZps.
proof: Proof. move => nN; apply/BZps_iP; split. apply:(BZ_of_natp_i (NS_pow NS2 nN)). move/(f_equal BZ_val); rewrite BZ0_val BZ_of_nat_val; apply: cpow_nz. exact: card2_nz. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)