proposition: Lemma order_modn_mod k m : 1 < k -> order_modn k (m %% k) = order_modn k m.
proof: Proof. move=> k_gt1. have [kCm| kNCm]:= boolP (coprime k m); last first. have kNCmk : ~~ coprime k (m %% k) by rewrite coprime_modr. by rewrite /order_modn coprime_sym (negPf kNCmk) coprime_sym (negPf kNCm). have kCmk : coprime k (m %% k) by rewrite coprime_modr. have [m_gt0 Hm Hmn] := order_modnP k_gt1 kCm. have [mk_gt0 Hmk Hmkn] := order_modnP k_gt1 kCmk. case: (leqP (order_modn k (m %% k)%N) (order_modn k m)) => [|mLmk]. rewrite leq_eqVlt => /orP[/eqP->//|mkLm]. have /Hmn/eqP[] : 0 < order_modn k (m %% k) < order_modn k m. by rewrite mk_gt0. by rewrite -modnXm. have /Hmkn/eqP[] : 0 < order_modn k m < order_modn k (m %% k). by rewrite m_gt0. by rewrite modnXm. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)