proposition: Lemma PCM_altP (x : 'rV_n) : (syndrome (BCH.PCM a t) (F2_to_GF2 m x) == 0) = (syndrome (BCH.PCM_alt a t) (F2_to_GF2 m x) == 0).
proof: Proof. apply/idP/idP. - rewrite /BCH.PCM /BCH.PCM_alt /syndrome => H. suff H' : forall j : 'I_t.*2, \sum_j0 (GF2_of_F2 (x ``_ j0) * (a ``_ j0) ^+ j.+1) = 0. apply/eqP/rowP => j; rewrite !mxE. rewrite -[RHS](H' j). apply eq_bigr => /= i _. by rewrite !mxE mulrC. move=> j. apply BCH_PCM_altP1 => i. move/eqP/rowP : H => /(_ i). rewrite !mxE => H; rewrite -[RHS]H. apply eq_bigr => /= k _; by rewrite !mxE /= mulrC. - rewrite /BCH.PCM_alt /BCH.PCM /syndrome => H. apply/eqP/rowP => i. have @j : 'I_t.*2. refine (@Ordinal _ i.*2 _); by rewrite -!muln2 ltn_pmul2r. move/eqP : H => /matrixP/(_ ord0 j). rewrite !mxE => {2}<-. apply eq_bigr => k _. by rewrite !mxE. 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