proposition: Lemma RS_min_dist : n.-primitive_root a -> min_dist (RS_not_trivial a dn) = d.+1.
proof: Proof. move=> na. apply min_distP; split; first by move=> *; apply RS_min_dist1. exists (poly_rV \gen_(a, d)); split; first by rewrite mem_rs_gen_RS. apply/andP; rewrite wH_rs_gen andbT. apply: contra (gen_neq0 a d). move/poly_rV_0_inv; apply; by rewrite size_rs_gen. 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