proposition: Lemma BCH_err_is_correct (a_not_uroot : not_uroot_on a n) l (e y : 'rV_n) : let r0 := 'X^t.*2 : {poly F} in let r1 := \BCHsynp_(rVexp a n, y, t) in let vj := Euclid.v r0 r1 (stop t r0 r1) in l <> 0 -> vj = l *: \sigma_(rVexp a n, F2_to_GF2 m e) -> e = poly_rV (BCH_err y).
proof: Proof. have H1 := distinct_non_zero_rVexp a_neq0 a_not_uroot. move=> r0 r1 vj /eqP l0 Hvj; apply/rowP => i. set r_ := \BCHomega_(rVexp a n, twisted a (F2_to_GF2 m e)). rewrite !mxE coef_poly ltn_ord; case: ifPn. rewrite -/r0 -/r1 -/r_ -/vj Hvj. rewrite !hornerZ !mulf_eq0 invrM; last 2 first. by rewrite unitfE. by rewrite unitfE horner_errloc_0 oner_neq0. rewrite mulf_eq0 !invr_eq0 (negbTE l0) /= orbF horner_errloc_0 oner_eq0 /=. move: (errloc_zero (supp (F2_to_GF2 m e)) i H1); rewrite mxE => ->. by rewrite supp_F2_to_GF2 inE -F2_eq1 => /eqP. rewrite -/r0 -/vj in Hvj *. rewrite Hvj !hornerZ !mulf_eq0 invrM; last 2 first. by rewrite unitfE. by rewrite unitfE horner_errloc_0 oner_neq0. rewrite mulf_eq0 !invr_eq0 (negbTE l0) /= orbF horner_errloc_0 oner_eq0 /=. move: (errloc_zero (supp (F2_to_GF2 m e)) i H1); rewrite mxE => ->. by rewrite supp_F2_to_GF2 inE negbK => /eqP ->. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv finalg zmodp) mathcomp(matrix mxalgebra mxpoly vector fieldext finfield) ssralg_ext hamming linearcode decoding cyclic_code poly_decoding vandermonde dft euclid grs f2