proposition: Lemma sumpow2_N2 n a K: natp n -> inc K (\Po (n -s1 a)) -> natp (sumpow2 K).
proof: Proof. move => nN /setP_P h1; move:(sub_trans h1 (@sub_setC _ _)) => h2. have h3:= (sub_trans h2 (NS_inc_nat nN)). exact (sumpow2_N1 (sub_finite_set h2 (finite_set_nat nN)) h3). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)