proposition: Lemma sumpow2_N1 K: finite_set K -> sub K Nat -> natp (sumpow2 K).
proof: Proof. move => ha hb; apply:finite_sum_finite; saw. hnf;aw => x xk; rewrite LgV//; apply:(NS_pow NS2 (hb _ xk)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)