proposition: Lemma F24 n: n > 0 -> \sum_(i<n.+1 | odd i) ( 'C(n, i)) = 2 ^ (n.-1).
proof: Proof. move => np. have: \sum_(i < n.+1) 'C(n, i) = 2 ^ (n.-1) * 2. by rewrite - expnSr (prednK np) pascal11. rewrite (bigID (fun i : 'I_n.+1 => odd i)) /= (F24_b np). by move /eqP; rewrite addnn - muln2 (eqn_pmul2r (ltn0Sn 1)); move /eqP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)