proposition: Lemma order_modn_exp k m : 1 < k -> coprime k m -> m ^ order_modn k m = 1 %[mod k].
proof: Proof. by move=> k_gt1 kCm; case: (order_modnP k_gt1 kCm). Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)