proposition: Lemma repcode_not_empty r (f : repairT _ _ _) (Hf : oimg f \subset Rep.code r) : {c | c \in Encoder.enc (Lcode.enc (Rep.Lcode_wo_repair Hf)) @: 'rV_ _}.
proof: Proof. by exists 0; apply/imsetP; exists (const_mx 0) => //; rewrite /= Rep.encodeE. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) hamming num_occ ssralg_ext f2 linearcode decoding channel_code