proposition: Lemma binomial_theorem m p : \sum_(b in [set: 'rV['F_2]_m]) (1 - p) ^ (m - wH b) * p ^ wH b = 1.
proof: Proof. transitivity (((1 - p) + p) ^ m); last by rewrite subRK exp1R. rewrite RPascal. transitivity (\sum_(b : 'rV['F_2]_m) (1 - p) ^ (m - wH b) * p ^ wH b). by apply eq_bigl => /= i; rewrite inE. rewrite sumRE (classify_big (fun s => Ordinal (max_wH' s)) (fun x => (1 - p) ^ (m - x) * p ^ x)) /=. apply: eq_bigr=> i _. rewrite -wH_m_card !coqRE; congr (_ %:R %mcR * _). by apply eq_card => /= x; rewrite !inE. Qed.
imports: Reals mathcomp(all_ssreflect fingroup zmodp ssralg finalg perm matrix) mathcomp(poly mxalgebra mxpoly) mathcomp(Rstruct) ssr_ext ssralg_ext f2 num_occ natbin ssrR Reals_ext bigop_ext