proposition: Lemma fiblist_res n: natp n -> fib_listsAc n = Fib (n +c \2c).
proof: Proof. move => nN. suff: fib_listsAc n = Fib (n +c \2c) /\ fib_listsBc n = Fib (n +c \1c). by case. move: n nN; apply: Nat_induction. rewrite fiblist_res3 fiblist_res4 (csum0l CS2) (csum0l CS1). by rewrite Fib1 Fib2. move => n nN [ha hb];split. rewrite - succ_one (csum_nS _ NS1) - (Nsucc_rw (NS_succ nN)). rewrite (Fib_rec (NS_succ nN)) csumC fiblist_res2 // ha hb. by rewrite - succ_one (csum_nS _ NS1) - (Nsucc_rw nN). by rewrite - fiblist_res1 // (csum_Sn _ nN) - (csum_nS _ NS1) succ_one. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)