proposition: Lemma fusc_pred_pow2 n: natp n -> fusc (\2c ^c n -c \1c) = n.
proof: Proof. move: n;apply: Nat_induction; first by rewrite cpowx0 cdiff_nn fusc0. move => n nN Hr. have pN: natp (\2c ^c n) by fprops. have pnz: (\2c ^c n) <> \0c by apply: (cpow_nz card2_nz). have [sa sb]:=(cpred_pr pN pnz). have sc := (cpred_pr4 (CS_nat pN)). have ->: (\2c ^c csucc n -c \1c) = csucc (cdouble (\2c ^c n -c \1c)). rewrite -(cdouble_pow2 nN) {1} sb - sc -/(cdouble _) (double_succ sa). rewrite - cpred_pr4; [rewrite cpred_pr1 //; apply: CS_succ | apply: CS_succ]. by rewrite (fusc_odd(NS_diff _ pN)) Hr - sc - sb (fusc_pow2 nN) (Nsucc_rw nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)