proposition: Lemma min_dist_achieved : exists c, c \in C /\ c <> 0 /\ wH c = min_dist.
proof: Proof. exists min_wH_cw; split. rewrite /min_wH_cw /=. case: arg_minnP => /=. by rewrite non_0_cw_mem wH_non_0_cw. by move=> /= c /andP[]. split; last reflexivity. rewrite /min_wH_cw /=. case: arg_minnP => /=. by rewrite non_0_cw_mem wH_non_0_cw. by move=> /= c /andP[_ /negP]; rewrite wH_eq0 => /negP/eqP. 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