proposition: Lemma min_dist_prop m m' : m \in C -> m' \in C -> m != m' -> min_dist <= dH m m'.
proof: Proof. move=> /= mm' mC m'C; apply min_dist_is_min. by apply Lcode0.aclosed => //; rewrite Lcode0.oclosed. by rewrite subr_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