proposition: Lemma RS_MDS : n.-primitive_root a -> maximum_distance_separable (RS_not_trivial a dn).
proof: Proof. move=> an. rewrite /maximum_distance_separable RS_min_dist // addn1 dim_RS_code //. - by rewrite subKn // ltnW. - exact: primitive_uroot_neq0 an. - by apply prim_root_not_uroot_on. 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