proposition: Lemma fusc_pow2 n: natp n -> fusc (\2c ^c n) = \1c.
proof: Proof. move: n; apply: Nat_induction; first by rewrite cpowx0 fusc1. move => n nN Hred; rewrite -(cdouble_pow2 nN). by rewrite (fusc_even (NS_pow NS2 nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)