proposition: Lemma RS_repair_output_is_in_the_code (x y : 'rV_n) (an1 : a ^+ n = 1) : RS_repair a _ d x = Some y -> y \in RS.code a n d.
proof: Proof. rewrite /RS_repair ffunE. case: ifPn => [|_]. rewrite RS.RS_syndromep_codeword // -RS.lcode0_codebook // inE. by move=> ? [<-]. case: ifPn => [|//]. rewrite RS.RS_syndromep_codeword // -RS.lcode0_codebook // inE => ?. by case=> <-. 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