proposition: Lemma sum_diag_pascal n: natp n -> csumb (Nintc n) (fun k => binom (n -c k) k) = Fib (csucc n).
proof: Proof. move => nN. rewrite (NintcE nN). move: clt_01 => clt01. have i01: inc \0c \1c by apply: set1_1. move:n nN {- 2} n (cleR (CS_nat nN)); apply: Nat_induction. move => n /cle0 ->; rewrite succ_zero Fib1 /csumb. set F := Lg _ _. have df:domain F = singleton \0c by rewrite/F;aw. have eq1: Vg F \0c = \1c by rewrite /F LgV//; rewrite cdiff_nn (binom0 NS0). rewrite (csum_trivial2 df) // eq1; fprops. move => n nN Hrec m lemn; case: (equal_or_not m (csucc n)) => eqmn; last first. by apply: Hrec; apply /(cltSleP nN). rewrite eqmn; case: (equal_or_not n \0c) => en0. rewrite en0 succ_zero succ_one Fib2. rewrite - succ_one (fct_sum_rec1 _ NS1) /csumb; set F := Lg _ _. have df: domain F = singleton \0c by rewrite /F; aw. have hb: \0c <c csucc \0c by rewrite succ_zero; apply:clt_01. have pa: Vg F \0c = \0c. rewrite /F (LgV i01) succ_zero cdiff_nn (binom_bad NS0 NS1) //. have pb: cardinalp(Vg F \0c) by rewrite pa; fprops. rewrite (csum_trivial2 df pb) pa (cdiff_n0 NS1) (binom0 NS1). by rewrite (Nsum0l NS1). move: (cpred_pr nN en0) => [sa sb]. rewrite (fct_sum_rec1 _ (NS_succ nN)). rewrite (induction_on_sum _ nN). rewrite cdiff_nn (binom_bad NS0 (NS_succ nN) (succ_positive n)). rewrite csum0r; last by apply: CS_csum. have hb: forall i, inc i n -> binom (csucc n -c csucc i) (csucc i) = binom (n -c csucc i) (csucc i) +c binom (cpred n -c i) i. move => i iI; move/(NltP nN): iI => lt1. have iN := (NS_lt_nat lt1 nN). have hb: csucc i <=c n by apply /(cleSltP iN). rewrite (cdiff_pr6 nN iN) (csucc_diff nN iN hb) - (cdiff_pr6 sa iN) - sb. by rewrite (binomSnSm (NS_diff (csucc i) nN) iN). rewrite /csumb (Lg_exten hb) - /(csumb _ _) - sum_of_sums. have ->: binom (csucc n -c \0c) \0c = binom (csucc (cpred n) -c \0c) \0c. rewrite - sb !binom0 //; fprops. rewrite {3} sb (Hrec _ (cpred_le (CS_nat nN))) - sb (csumC _ (Fib n)) - csumA. rewrite {2} sb - (fct_sum_rec1 (fun i=> binom (n -c i) i) (NS_succ sa)). by rewrite - sb (Fib_rec nN) (Hrec _ (cleR (CS_nat nN))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)