proposition: Lemma min_dist_is_min c : c \in C -> c != 0 -> min_dist <= wH c.
proof: Proof. move=> cC c0; rewrite /min_dist /min_wH_cw. case: arg_minnP => /= [|c1 /andP [] Hc1 wHc1]. by rewrite non_0_cw_mem wH_non_0_cw. by apply; rewrite cC /= wH_eq0. 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