proposition: Lemma sumpow2_rec a K: inc a K -> sumpow2 K = sumpow2 (K -s1 a) +c (\2c ^c a).
proof: Proof. by move=> aK; rewrite -{1} (setC1_K aK) /sumpow2 (csumA_setU1 _ (@setC1_1 a K)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)