proposition: Lemma order_modnP m n : 1 < m -> coprime m n -> [/\ 0 < order_modn m n, (n ^ order_modn m n = 1 %[mod m])%N & (forall j, 0 < j < order_modn m n -> n ^ j != 1 %[mod m])%N].
proof: Proof. move=> m_gt1 mCn. rewrite /order_modn m_gt1 coprime_sym mCn /=. apply: order_modn_recP => //; first by rewrite coprime_sym. - by case. - by rewrite modn_small. by rewrite addn1. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)