proposition: Lemma order_modn_dvd k m : 1 < k -> coprime k m -> (k %| (m ^ order_modn k m).-1)%N.
proof: Proof. move=> k_gt1 kCm. have /(order_modnP k_gt1)[o_gt0 /eqP] := kCm. rewrite /dvdn [(1 %% _)%N]modn_small // => /eqP modE _. by rewrite (divn_eq (_ ^ _) k) modE addn1 /= modnMl. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)