proposition: Lemma card_dH_vec (x y : 'rV['F_2]_n) : (#| [pred i | y ``_ i != x ``_ i ] |)%N = dH x y.
proof: Proof. rewrite /dH wH_num_occ num_occ_alt /=. apply eq_card => /= i. rewrite inE. move H : (_ \in _) => [|]. symmetry. rewrite F2_eq1. apply: contra H. by rewrite tnth_mktuple !mxE subr_eq0 eq_sym. move/negbT in H. rewrite negbK in H. apply/esym/negbTE. rewrite -F2_eq0 tnth_mktuple !mxE. move/eqP : H => ->. by rewrite subr_eq0. 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