proposition: Lemma F25 n: n > 0 -> \sum_(i<n.+1 | ~~ odd i) 'C(n, i) = 2 ^ (n.-1).
proof: Proof. by move => np; rewrite (F24_b np) F24. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)