proposition: Lemma wH_vproj_take n (F : ringType) (x : 'rV[F]_n) t : wH (vproj x [set i in take t (enum (wH_supp x))]) <= t.
proof: Proof. set s := take t (enum (wH_supp x)). rewrite (leq_trans (wH_vproj x [set i in s])) //. apply (@leq_trans (size s)); last first. rewrite size_take -cardE card_wH_supp; case: ifPn => //; by rewrite -leqNgt. rewrite cardsE; apply/eq_leq/card_uniqP. have : subseq s (enum (wH_supp x)). by rewrite -(cat_take_drop t (enum (wH_supp x))) prefix_subseq. move/subseq_uniq; apply; by apply enum_uniq. 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