proposition: Lemma uniq_roots_exp : uniq_roots [seq a ^+ i | i <- iota 1 d].
proof: Proof. rewrite uniq_rootsE map_inj_in_uniq; first by rewrite iota_uniq. move=> i j. rewrite !mem_iota addnC addn1 => H1. move: H1 => // /andP[_ Hid] /andP [_ Hjd] /eqP aij. apply/eqP. by rewrite (val_eqE (Ordinal (leq_trans _ dn)) (Ordinal (leq_trans _ dn))) -(exp_inj a_neq0). 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