proposition: Lemma rep_encode_decode m v : m \in LC -> let enc := Lcode.enc LC in let rep := Decoder.repair (Lcode.dec LC) in rep v != None -> dH m v <= mdd_err_cor (not_trivial_replcode (@reprepair_img r)) -> rep v = Some m.
proof: Proof. move=> Hm enc dec H1 H2. apply: (@mddP _ _ _ _ (@repcode_MD_decoding r) (not_trivial_replcode (@reprepair_img r)) ) => //=. exact: reprepair_img. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) hamming num_occ ssralg_ext f2 linearcode decoding channel_code