proposition: Lemma reprepair_img r : oimg (@repair r) \subset Rep.code r.
proof: Proof. apply/subsetP => y. rewrite inE => /existsP [x]. rewrite mem_kernel_syndrome0 /repair /majority_vote ffunE; case: ifPn => [_ /eqP [<-]|_]. by rewrite -mem_kernel_syndrome0 Rep.const_mx_in_code. case: ifPn => // _ /eqP [<-]. by rewrite -mem_kernel_syndrome0 mem0v. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) hamming num_occ ssralg_ext f2 linearcode decoding channel_code