proposition: Lemma order_modn_gt1 k m : 1 < order_modn k m -> 1 < k.
proof: Proof. by rewrite /order_modn andbC; case: (1 < k). Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)