proposition: Lemma fusc_rec_spec n i (q := \2c ^c n)(p := cdouble q) : natp n -> i <c q -> fusc i *c fusc(csucc p +c i) +c \1c = fusc (csucc i) *c fusc(p +c i).
proof: Proof. rewrite /p / q => nN lip {p q}. have iN:= (NS_lt_nat lip (NS_pow NS2 nN)). move: n nN i iN lip; apply: Nat_induction. rewrite cpowx0 => i _ /clt1 ->. rewrite fusc0 cprod0l (csum0l CS1) /cdouble (Nprod1r NS2). by rewrite (csum0r CS2) (succ_zero) fusc1 fusc2 (cprod1r CS1). move => n nN Hrec i iN. move: (NS_half iN);set k := (chalf i) => kN. have ha: natp (\2c ^c csucc n +c k) by fprops. have hb: natp (cdouble (\2c ^c csucc n)) by rewrite/cdouble;fprops. have hc: natp (cdouble (\2c ^c n)) by rewrite /cdouble;fprops. case: (cdouble_halfV iN) => -> lkn; rewrite -/k. rewrite (fusc_even kN) (fusc_odd kN) double_sum (fusc_even ha). rewrite (csum_Sn _ hb) double_sum (fusc_odd ha) cprodDl cprodDr - csumA. congr (_ +c _); rewrite - (cdouble_pow2 nN) - (csum_Sn _ hc). apply: (Hrec _ kN); apply /(double_monotone2 kN (NS_pow NS2 nN)). by rewrite (cdouble_pow2 nN). rewrite (fusc_odd kN) - (double_succ kN) (fusc_even (NS_succ kN)). rewrite (csum_Sn _ hb) (csum_nS _ (NS_double kN)) double_sum -(double_succ ha). rewrite (fusc_even (NS_succ ha)) (fusc_odd ha). rewrite cprodDl cprodDr (csumC _ \1c) csumA; apply:f_equal2; last exact. rewrite csumC. move: lkn; rewrite - (cdouble_pow2 nN) - (csum_Sn _ hc) => lkn. apply: (Hrec k kN); apply /double_monotone3; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)