proposition: Lemma card_dH (x y : n.-tuple 'F_2) : (#| [pred i | y !_ i != x !_ i ] |)%N = dH (row_of_tuple x) (row_of_tuple y).
proof: Proof. rewrite /dH wH_num_occ num_occ_alt /=. apply eq_card => /= i. rewrite inE. move H : (_ \in _) => [|]. symmetry. rewrite F2_eq1. move: H; apply contra. 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