proposition: Lemma min_dist_prop_old (M : finType) (C : t A B n M) (C_not_trivial : not_trivial C) m m' : m != m' -> min_dist C_not_trivial <= dH (Encoder.enc (enc C) m) (Encoder.enc (enc C) m').
proof: Proof. move=> /= mm'. have H : Encoder.enc (enc C) m - Encoder.enc (enc C) m' \in C. apply Lcode0.aclosed. - move/subsetP: (Encoder.enc_img (enc C)) => /(_ (Encoder.enc (enc C) m)). apply; apply/imsetP => /=; by exists m. - rewrite Lcode0.oclosed //. move/subsetP: (Encoder.enc_img (enc C)) => /(_ (Encoder.enc (enc C) m')). apply; apply/imsetP => /=; by exists m'. have H' : Encoder.enc (enc C) m - Encoder.enc (enc C) m' != 0. move: mm'; apply contra. rewrite subr_eq0. move/eqP. move/Encoder.enc_inj/eqP. by rewrite eqtype.eq_sym. by apply min_dist_is_min. 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