proposition: Lemma mdd_oddE : odd min_dist -> mdd_err_cor = min_dist./2.
proof: Proof. move=> odd_d. rewrite /mdd_err_cor (_ : _.-1./2 = min_dist./2) //. by rewrite -{1}(odd_double_half min_dist) odd_d /= (half_bit_double _ false). 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