proposition: Lemma min_distP d : (forall x : 'rV[F]_n, x \in C -> x != 0 -> d <= wH x) /\ (exists x : 'rV[F]_n, x \in C /\ x != 0 /\ wH x <= d) -> min_dist = d.
proof: Proof. case=> H1 [y [yC [y0 yd]]]. rewrite /min_dist /min_wH_cw. case: arg_minnP => /=. by rewrite non_0_cw_mem wH_non_0_cw. move=> x /andP[xC x0] H. apply/eqP. rewrite eqn_leq; apply/andP; split; last first. apply H1 => //; by rewrite -wH_eq0. by rewrite (leq_trans _ yd) // H // yC 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