proposition: Lemma mdd_err_cor_rep (Hr : odd r.+1) : mdd_err_cor not_trivial_replcode = r./2.
proof: Proof. by rewrite /mdd_err_cor min_dist_repcode // Hr. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) hamming num_occ ssralg_ext f2 linearcode decoding channel_code