proposition: Lemma RS_repair_img (an1 : a ^+ n = 1) (Hchar : ([char F]^').-nat n'.+1) : oimg (RS_repair a _ d) \subset RS.code a n d.
proof: Proof. apply/subsetP => /= y. rewrite inE => /existsP[/= x /eqP]. by apply RS_repair_output_is_in_the_code. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly vector mxalgebra zmodp) ssr_ext ssralg_ext poly_ext channel_code decoding linearcode hamming dft poly_decoding euclid grs cyclic_code