proposition: Lemma BCH_syndrome_synp y : t.*2 < n -> (syndrome (BCH.PCM (rVexp a n) t) (F2_to_GF2 m y) == 0) = (\BCHsynp_(rVexp a n, y, t) == 0).
proof: Proof. move=> tn. apply/idP/idP. - move/eqP/eqP. rewrite BCH.PCM_altP // /BCH.PCM_alt. move/eqP => K. rewrite /BCH.syndromep /syndromep. rewrite poly_def (eq_bigr (fun=> 0)) ?big_const ?iter_addr0 // => /= i _. apply/eqP; rewrite scaler_eq0. rewrite fdcoorE -size_poly_eq0 size_polyXn /= orbF. move/rowP : K => /(_ (inord i)) K. apply/eqP. rewrite !mxE in K. rewrite -[RHS]K. apply eq_bigr => k _. rewrite !mxE mulrC; congr (_ * _). rewrite -exprM mulnC exprM; congr (a ^+ _ ^+ _). by rewrite inord_val // inordK // (leq_ltn_trans (ltn_ord i)). - move=> K. apply/eqP; apply/eqP. rewrite BCH.PCM_altP //; apply/eqP. rewrite /BCH.PCM_alt. apply/rowP => i. rewrite !mxE. move/eqP: K. move/(congr1 (fun x : {poly F} => x`_i)). rewrite /BCH.syndromep /syndromep. rewrite coef0 poly_def coef_sum (bigD1 i) //= (eq_bigr (fun=> 0)); last first. move=> j ji. rewrite coefZ coefXn (_ : _ == _ = false) ?mulr0 //. by apply/negbTE; rewrite eq_sym. rewrite big_const iter_addr0 addr0 fdcoorE coefZ coefXn eqxx mulr1 => K. rewrite -[RHS]K. apply eq_bigr => k _. rewrite !mxE mulrC; congr (_ * _). by rewrite -exprM mulnC exprM inordK // (leq_ltn_trans _ tn). 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