proposition: Lemma order_modnE n m : 1 < m -> coprime m n -> order_modn m n = oapp (fingroup.order : {unit 'Z_m} -> nat) 0%N (insub n%:R).
proof: Proof. move=> m_gt1 mCn. case: insubP; rewrite unitZpE ?mCn //= => u _ Hu. have [o_gt0 moE1 Hmon] := order_modnP m_gt1 mCn. case: (leqP (order_modn m n) #[u]%g) => [|uLo]. rewrite leq_eqVlt => /orP[/eqP //|]. rewrite ltnNge => /negP[]. apply: dvdn_leq => //. rewrite cyclic.order_dvdn. apply/eqP/val_eqP => /=. by rewrite FinRing.val_unitX /= Hu -natrX -Zp_nat_mod // moE1 modn_small. have : n ^ #[u]%g != 1 %[mod m] by apply: Hmon; rewrite order_gt0. have /val_eqP/= := expg_order u. rewrite FinRing.val_unitX /= Hu -natrX -val_Zp_nat // => /eqP->. by rewrite modn_small. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)