proposition: Lemma BCH_PCM_altP1 (x : 'rV['F_2]_n) : (forall i : 'I_t, \sum_j GF2_of_F2 x ``_ j * a ``_ j ^+ i.*2.+1 = 0) -> (forall i : 'I_t.*2, \sum_j GF2_of_F2 x ``_ j * a ``_ j ^+ i.+1 = 0).
proof: Proof. move=> H [i]. elim: i {-2}i (leqnn i) => [|i IH j ji i1]. move=> i; rewrite leqn0 => /eqP -> i0. destruct t. exfalso; by rewrite -muln2 mul0n ltnn in i0. by rewrite -[RHS](H ord0); apply eq_bigr. case/boolP : (odd j) => [odd_j|even_j]; last first. have j2t : j./2 < t by rewrite -divn2 ltn_divLR // muln2. rewrite -[in RHS](H (Ordinal j2t)) /=. apply/eq_bigr => k _. move: (odd_double_half j). by rewrite (negbTE even_j) add0n => ->. move: (IH j.-1./2). rewrite -{1}divn2 leq_divLR; last first. rewrite dvdn2 -subn1 oddB; last by destruct j. by rewrite /= addbT odd_j. have -> : (j.-1 <= i * 2)%N. rewrite muln2 -addnn -subn1 leq_subLR addnA add1n (leq_trans ji) //. by rewrite addSn ltnS leq_addr. move/(_ isT). have j2t : (j.-1)./2 < t.*2. rewrite -divn2 ltn_divLR // -ltnS. destruct j => //. by rewrite /= (ltn_trans i1) // ltnS muln2 -[in X in _ <= X]addnn leq_addl. move/(_ j2t)/(congr1 (fun x => x ^+ 2)). rewrite expr0n /= sum_char2 ?char_GFqm // => H'. rewrite -[RHS]H'; apply eq_bigr => k _. rewrite exprMn_comm; last by rewrite /GRing.comm mulrC. congr (_ * _); last first. rewrite /= -exprM muln2; congr (_ ^+ _). move: (odd_double_half j). rewrite odd_j add1n => <-. by rewrite (half_bit_double (j./2) false) -doubleS. by rewrite (expr2 (GF2_of_F2 x ``_ k)) -rmorphM -expr2 f2.expr2_char2. 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