proposition: Lemma min_dist_repcode (Hr : odd r.+1) : min_dist not_trivial_replcode = r.+1.
proof: Proof. rewrite /min_dist /= (_ : min_wH_cw _ = const_mx 1) ?wH_const_mx //. rewrite /min_wH_cw. case: arg_minnP => /=. rewrite non_0_codeword_replcode (Rep.const_mx_in_code r 1) /= wH_eq0 /=. by apply/eqP => /matrixP/(_ 0 0); rewrite !mxE. move=> i Hi _. have {Hi} : i \in Rep.Lcode_wo_repair Hf /\ wH i != O by split; case/andP : Hi. move/setP: (Rep.codewords r) => /(_ i). rewrite !inE => -> -[] /orP [/eqP // | /eqP ->]. by rewrite wH0 eqxx. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) hamming num_occ ssralg_ext f2 linearcode decoding channel_code