proposition: Lemma fusc_kpow2n k n : natp n -> natp k -> fusc (\2c ^c n *c k) = fusc k.
proof: Proof. move => nN kN; move: n nN; apply: Nat_induction. by rewrite cpowx0 (cprod1l (CS_nat kN)). move => n nN Hrec. rewrite (cpow_succ _ nN) (cprodC _ \2c) - cprodA fusc_even;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)