proposition: Lemma dH_vproj n (F : ringType) (x : 'rV[F]_n) (s : {set 'I_n}) : s \subset wH_supp x -> dH x (vproj x s) = #| (~: s) :&: (wH_supp x) |.
proof: Proof. move=> H; rewrite dHE. have -> : x - vproj x s = vproj x (~: s). apply/rowP => i; rewrite !mxE !inE; case: ifPn => /=; [by rewrite subrr | by rewrite subr0]. rewrite /vproj /wH count_map /= cardE size_filter -enumT /=. apply eq_in_count => /= i _; rewrite !mxE !inE. case: ifPn => //; by rewrite eqxx. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv fingroup perm) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector) ssr_ext ssralg_ext poly_ext f2 hamming decoding channel_code