proposition: Lemma csum_fusc_row n: natp n -> csumb (interval_co Nat_order (\2c ^c n) (\2c ^c (csucc n))) fusc = \3c ^c n.
proof: Proof. move => nN. have ->: csumb(interval_co Nat_order (\2c ^c n) (\2c ^c (csucc n))) fusc = csumb (Nint (\2c ^c n)) (fun z => fusc (z +c (\2c ^c n))). move: (NS_pow NS2 nN) => ha. have hha := NS_sum ha ha. rewrite - (cdouble_pow2 nN) /cdouble - csum_nn. apply: csum_Cn2; split. + move => x /(NintP ha) len. move:(NS_lt_nat len ha) => xN; move:(NS_sum xN ha) => sn. have hc:= (NS_pow NS2 (NS_succ nN)). have hb: \2c ^c n <=c x +c \2c ^c n by apply:csum_Mle0;fprops. apply/Nint_coP1 => //. by move:(csum_Mlteq ha len) => [pa pb]. + by move => x y /Nint_S1 xN /Nint_S1 yN; apply:csum_eq2r. + move => y /Nint_coP [[_ pa pb] [[_ pc pd] pe]]; move: (cdiff_pr pb) => hd. exists (y -c ( \2c ^c n)) ; last by rewrite csumC hd. apply /(NintP ha);rewrite - {1} hd in pd. have pf: \2c ^c n +c (y -c \2c ^c n) <> \2c ^c n +c \2c ^c n by ue. exact:(csum_lt2l ha (NS_diff (\2c ^c n) pa) ha (conj pd pf)). move: n nN; apply: Nat_induction. rewrite ! cpowx0 (proj2 Nint_co01) /csumb. set F1 := Lg _ _; have ha: (domain F1 = singleton \0c) by rewrite /F1; aw. rewrite (csum_trivial1 ha) /F1 (LgV (set1_1 \0c)). by rewrite (csum0l CS1) fusc1(card_card CS1). move => n nN Hrec. have ha := (NS_pow NS2 nN). rewrite (split_sum_even_odd_alt _ (NS_pow NS2 (NS_succ nN))). rewrite - (cdouble_pow2 nN) (even_half ha) (odd_half ha). have ->: csumb (Nint (\2c ^c n)) (fun k => fusc (cdouble k +c cdouble (\2c ^c n))) = csumb (Nint (\2c ^c n)) (fun k => fusc (k +c (\2c ^c n))). apply: csumb_exten => i /Nint_S1 iN. rewrite double_sum; apply: fusc_even; fprops. have ->: csumb (Nint (\2c ^c n)) (fun k => fusc (csucc (cdouble k) +c cdouble (\2c ^c n))) = csumb (Nint (\2c ^c n)) (fun k => fusc (k +c \2c ^c n) +c fusc ((csucc k) +c (\2c ^c n))). apply: csumb_exten => i /Nint_S1 iN. rewrite (csum_Sn _ (NS_double iN)) double_sum (fusc_odd (NS_sum iN ha)). by rewrite - (csum_Sn _ iN). suff H: csumb (Nint (\2c ^c n)) (fun i => fusc (csucc i +c \2c ^c n)) = csumb (Nint (\2c ^c n)) (fun i => fusc (i +c \2c ^c n)). rewrite - sum_of_sums H ! Hrec csum_nn csumC cprodC -(cprod_nS _ NS2). by rewrite (cpow_succ _ nN). have hb: (\2c ^c n) <> \0c by apply cpow_nz; apply : card2_nz. move:(cpred_pr ha hb) => [sa sb]. have hc: (Nint (\2c ^c n)) = (Nintc (cpred (\2c ^c n))). by rewrite {1} sb - (Nint_co_cc sa). symmetry. rewrite {1} hc (fct_sum_rec0 _ sa) (Nsum0l ha) (fusc_pow2 nN). rewrite (NintE ha) {3} sb (induction_on_sum _ sa) - sb csum_nn. rewrite - /(cdouble _) (cdouble_pow2 nN) (fusc_pow2 (NS_succ nN)). congr (_ +c \1c);apply:csum_Cn2; split. + move => x /(NltP sa) hd; apply /(Nint1cP sa); split;first by apply: succ_nz. by apply /(cleSltP (NS_lt_nat hd sa)). + move => x y /(NS_inc_nat sa) xN /(NS_inc_nat sa) yN. apply /csucc_inj; fprops. + move => y /(Nint1cP sa) [ya yb]; move:(NS_le_nat yb sa) => yN. move:(cpred_pr yN ya) => [sc eq1]; exists (cpred y) => //. by apply /(NltP sa); apply/(cleSltP sc); rewrite - eq1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)