proposition: Lemma fusc_mean_div n p (b := (\2c ^c n) *c csucc (cdouble p)) (a := cpred b) (c := csucc b): natp n -> natp p -> fusc a +c fusc c = (fusc b) *c csucc (cdouble n).
proof: Proof. rewrite /a /c /b => nN pN; move: n nN {a b c}; apply: Nat_induction. move: (NS_double pN) => dN; move:(NS_succ dN) => sdN. rewrite cpowx0 (Nprod1l sdN) (cpred_pr1 (CS_nat dN)) (fusc_even pN). rewrite - (double_succ pN) (fusc_even (NS_succ pN))- (fusc_odd pN). by rewrite cdouble0 succ_zero (Nprod1r (NS_fusc sdN)). move => n nN. rewrite - (cdouble_pow2 nN) cprodC (cprodC (cdouble (\2c ^c n))). rewrite double_prod; set q:= _ *c _; move => Hrec. have dpN:= (NS_succ (NS_double pN)). have n2N:=(NS_pow NS2 nN). have qN:=(NS_prod dpN n2N). have qnz: q <> \0c by apply: cprod2_nz; [ apply: succ_nz | apply:cpow2_nz]. move: (cpred_pr qN qnz); rewrite -/ q; move => [sa sb]. have sc:cardinalp (csucc (cdouble (cpred q))) by apply: CS_succ. rewrite {1} sb (double_succ sa) (cpred_pr1 sc) (fusc_odd sa) - sb. rewrite (fusc_even qN) (fusc_odd qN) csumA -(csumA _ _ (fusc q)). rewrite csum_nn csumC csumA (csumC _ (fusc (cpred q))) Hrec. rewrite -(cprodC _ \2c) - cprodDr (csum_Sn _ (NS_double nN)) (Nsucc_rw nN). by rewrite - double_sum {4}/cdouble (Nprod1r NS2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)