proposition: Lemma card_dHC (x y : 'rV['F_2]_n) : (#| [pred i | y ``_ i == x ``_ i ] |)%N = (n - dH x y)%nat.
proof: Proof. move: (cardC [pred i | y ``_i == x ``_i ]). rewrite card_ord => H. by rewrite -[in X in _ = (X - _)%nat]H -card_dH_vec -addnBA // subnn addn0. 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