proposition: Lemma bin_sum_diag: forall n, \sum_(i < n) 'C(n.-1-i,i) = fib n.
proof: Proof. move=> n; elim: n {-2}n (leqnn n)=> [[] // _ |n IH]; first by rewrite big_ord0. move=> n1; rewrite leq_eqVlt; case/orP=> [|Hn]; last first. by apply: IH; rewrite -ltnS. move/eqP->; case: n IH=> [|[|n]] IH. - by rewrite big_ord_recr big_ord0. - by rewrite !big_ord_recr big_ord0. rewrite fibSS -!IH // big_ord_recl bin0 big_ord_recr /= subnn bin0n addn0. set ss := \sum_(i < _) _. rewrite big_ord_recl bin0 -addnA -big_split; congr (_ + _). by apply eq_bigr=> i _ /=; rewrite -binS subSn //; case: i. Qed.
imports: mathcomp(all_ssreflect all_algebra)