proposition: Lemma min_dist_neq0 : min_dist <> O.
proof: Proof. move=> abs. case: min_dist_achieved => /= v [vC [/eqP/eqP v0]]. by rewrite abs; move/eqP; rewrite wH_eq0 => /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