proposition: Lemma RS_key_equation y : \sigma_(rVexp a n, y) * \RSsynp_(rVexp a n, y, t) = \RSomega_(rVexp a n, y) + - RS_mod y t * 'X^t.
proof: Proof. move: (@RS_GRS_syndromep F n' a t y tn) => H0. move: (GRS_key_equation y (rVexp a n) (rVexp a n) t). rewrite -{}H0 => ->; by rewrite RS_mod_is_GRS_mod opprK. 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