proposition: Lemma BCH_PCM_altP2 (x : 'rV[F]_n) : (forall i : 'I_t.*2, \sum_j x ``_ j * a ``_ j ^+ i.+1 = 0) -> (forall i : 'I_t,\sum_j x ``_ j * a ``_ j ^+ i.*2.+1 = 0).
proof: Proof. move=> H i. have @j : 'I_t.*2 by refine (@Ordinal _ i.*2 _); rewrite -!muln2 ltn_pmul2r. rewrite -[RHS](H j); by apply eq_bigr => /= k _. 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