proposition: Lemma codebook_syndrome (c : 'rV_n) : (c \in codebook) = (syndrome (PCM a n d) c == 0).
proof: Proof. rewrite syndrome_syndromep inE; apply/idP/idP. - move/forallP => H; apply/eqP/rowP => i; rewrite !mxE. rewrite /syndromep /poly_decoding.syndromep poly_def coef_sum. rewrite (eq_bigr (fun=> 0)) ?big_const ?iter_addr0 // => j _. rewrite coefZ; apply/eqP; rewrite mulf_eq0. have @j' : 'I_d.+1. by apply (@Ordinal _ j.+1); move: (ltn_ord j); rewrite -ltnS. move: (H j'); by rewrite lt0n /= => ->. - move/eqP/rowP => H. apply/forallP => /= i; apply/implyP => i0. have @i' : 'I_d. apply (@Ordinal _ i.-1). by rewrite prednK // -ltnS. move: (H i'); rewrite !mxE. rewrite /syndromep /poly_decoding.syndromep. rewrite coef_poly ltn_ord => /eqP /=. by rewrite prednK. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly vector mxalgebra zmodp) ssr_ext ssralg_ext poly_ext channel_code decoding linearcode hamming dft poly_decoding euclid grs cyclic_code