proposition: Lemma wH_vproj_take2 n (F : ringType) (x : 'rV[F]_n) t : t < wH x <= t.*2 -> dH x (vproj x [set i in take t (enum (wH_supp x))]) <= t.
proof: Proof. move=> xt. rewrite dH_vproj; last first. apply/subsetP => i /=; rewrite !inE. by move/mem_take; rewrite mem_enum inE. rewrite (@leq_trans #| drop t (enum (wH_supp x)) |) //. apply/subset_leq_card/subsetP => /= i. rewrite !inE => /andP[] si xi0. have : i \in enum (wH_supp x) by rewrite mem_enum inE. rewrite -{1}(cat_take_drop t (enum (wH_supp x))) mem_cat => /orP[] //. by rewrite (negbTE si). have : #| wH_supp x | <= t.*2 by rewrite card_wH_supp; case/andP : xt. rewrite cardE -{1}(cat_take_drop t (enum (wH_supp x))). rewrite size_cat -addnn size_take -{1}cardE card_wH_supp. case/andP : xt => -> /= _. rewrite leq_add2l; apply/leq_trans/eq_leq/card_uniqP. have : uniq (enum (wH_supp x)) by apply enum_uniq. by rewrite -{1}(cat_take_drop t (enum (wH_supp x))) cat_uniq => /and3P[]. 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