proposition: Lemma Fib_add n m: natp n -> natp m -> Fib (csucc (n +c m)) = (Fib n) *c (Fib m) +c (Fib (csucc n)) *c (Fib (csucc m)).
proof: Proof. move => nn;move: n nn m; apply: Nat_induction. move => m mN; move:(CS_nat (NS_Fib (NS_succ mN))) => cf. by rewrite (Nsum0l mN) succ_zero Fib0 Fib1 cprod0l (cprod1l cf) csum0l. move => n nN Hrec m mN. case: (equal_or_not m \0c) => mz. move:(CS_nat (NS_Fib (NS_succ (NS_succ nN)))) => cf. rewrite mz succ_zero Fib0 Fib1 cprod0r (cprod1r cf) (csum0l cf) csum0r;fprops. move:(cpred_pr mN mz) => [sa sb]. rewrite (csum_Sn _ nN) (Fib_rec (NS_sum nN mN)) (Fib_rec nN) (Hrec _ mN). rewrite cprodDl csumA csumA {1} sb (csum_nS _ sa) (Hrec _ sa) - sb. apply:f_equal2; last by reflexivity. rewrite csumC csumA (csumC (_ *c _)). by rewrite - cprodDr {2} sb - (Fib_rec sa) - sb csumC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)