proposition: Lemma RS_GRS_syndromep y : RS.redundancy_ub d n -> \RSsynp_(b, y, d) = (GRS.syndromep b b d) y.
proof: Proof. move=> dn; rewrite /GRS.syndromep /poly_decoding.syndromep. apply/polyP => i. rewrite 2!coef_poly; case: ifP => // id1. by rewrite fdcoor_GRS_syndrome_coor // (leq_trans id1). 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