proposition: Lemma wH_vproj n (F : ringType) (x : 'rV[F]_n) (s : {set 'I_n}) : wH (vproj x s) <= #| s |.
proof: Proof. rewrite /wH count_map (_ : #| s | = count (mem s) (enum 'I_n)); last first. rewrite cardE -count_predT !count_filter; apply eq_in_count => /= i _. by rewrite !inE andbT. apply sub_count => /= i /=. rewrite mxE; 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