proposition: Lemma NS_pow a b: natp a -> natp b -> natp (a ^c b).
proof: Proof. move=> aN bN. move: b bN; apply: Nat_induction; first by rewrite cpowx0; fprops. by move=> n nN mN; rewrite cpow_succ => //;apply: NS_prod. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)