proposition: Lemma RS_err_is_correct l (e y : 'rV_n) : distinct_non_zero (rVexp a n) -> let r0 := 'X^d : {poly F} in let r1 := \RSsynp_(rVexp a n, y, d) in let vj := Euclid.v r0 r1 (stop (odd d + t) r0 r1) in let rj := Euclid.r r0 r1 (stop (odd d + t) r0 r1) in l <> 0 -> vj = l *: \sigma_(rVexp a n, e) -> rj = l *: \RSomega_(rVexp a n, e) -> e = poly_rV (RS_err a d y).
proof: Proof. move=> H1 r0 r1 vj rj /eqP l0 Hvj Hrj; apply/rowP => i. rewrite mxE coef_poly ltn_ord -/r0 -/r1 -/vj -/rj; case: ifPn => H. apply: (@mulIf _ ((rVexp a n) ``_ i)). by rewrite mxE expf_eq0 negb_and a_neq0 orbT. rewrite (erreval_vecE H1 (rVexp a n)) //; last first. rewrite -(errloc_zero _ _ H1) mxE. move: H; rewrite Hvj !hornerZ !mulrA mulf_eq0 => /orP[|//]. rewrite mulf_eq0 (negbTE l0) orbF invr_eq0 mulf_eq0 (negbTE l0) orFb. by rewrite horner_errloc_0 oner_eq0. rewrite 2![in RHS]mulNr -[in RHS]mulrN [in RHS]mulrC -mulrA; congr (_ * _). rewrite Hvj Hrj -/(\RSomega_(rVexp a n, e)) mxE !scalerA !(hornerZ,derivZ). set x := (_^-1 * _). rewrite -mulf_div divrr ?mul1r // unitfE mulf_neq0 //. by rewrite invr_neq0 // mulf_neq0 // horner_errloc_0 oner_neq0. apply/eqP; apply: contraNT H. rewrite -insupp -(errloc_zero _ _ H1) mxE Hvj !hornerZ => /eqP ->. by rewrite !mulr0. 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