proposition: Lemma encode_decode c y : c \in lcode -> repair y != None -> dH c y <= 1 -> repair y = Some c.
proof: Proof. move=> Hc Hy cy. apply: (@mddP _ _ lcode _ decoder (hamming_not_trivial r')) => //. by apply hamming_repair_img. by rewrite /mdd_err_cor hamming_min_dist. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) mathcomp(Rstruct) realType_ext ssr_ext ssralg_ext f2 linearcode natbin ssrR hamming bigop_ext fdist proba channel channel_code decoding binary_symmetric_channel