proposition: Lemma F24_a n: n > 0 -> \sum_(i<n) ( 'C(n, i.*2)) = \sum_(i<n) ('C(n, i.*2.+1)).
proof: Proof. case n; [by rewrite ltn0 | move => m _]. rewrite big_ord_recl bin0. rewrite [X in 1 + X] (_:_ = \sum_(i < m) ('C(m, i.*2.+2) + 'C(m, i.*2.+1))) //. transitivity (\sum_(i < m.+1) ('C(m, i.*2.+1) + 'C(m, i.*2))); last by []. rewrite big_split big_split /= addnA addnC; congr ( _ + _). rewrite big_ord_recr /= bin_small ?addn0 // ltnS -addnn; apply: leq_addr. rewrite big_ord_recl bin0 //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)