proposition: Lemma fusc_succ_pow2 n: natp n -> fusc (\2c ^c n +c \1c) = csucc n.
proof: Proof. move: n;apply: Nat_induction. by rewrite cpowx0 csum_11 fusc2 succ_zero. move => n nN Hr. have pN: natp (\2c ^c n) by fprops. rewrite -(cdouble_pow2 nN) - (Nsucc_rw (NS_double pN)) (fusc_odd pN). by rewrite (fusc_pow2 nN) (Nsucc_rw pN) Hr csumC - (Nsucc_rw (NS_succ nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)