proposition: Lemma hamming_repair_img : oimg hamming_repair \subset Hamming.code m.
proof: Proof. apply/subsetP => y /=. rewrite inE => /existsP[/= x]. rewrite /hamming_repair ffunE => /eqP [<-]. by rewrite mem_kernel_syndrome0 syndromeD syndrome_hamming_err F2_addmx. 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