proposition: Lemma order_modn_recP m n r i k : coprime n m -> 1 < m -> 0 < i -> (forall j, 0 < j < i -> (n ^ j != 1 %[mod m])%N) -> r = (n ^ i.-1 %% m)%nat -> m.+1 = (k + i)%nat -> [/\ 0%N < order_modn_rec m n r i k, (n ^ order_modn_rec m n r i k = 1 %[mod m])%N & (forall j, 0 < j < order_modn_rec m n r i k -> (n ^ j != 1 %[mod m])%N)].
proof: Proof. move=> nCm m_gt1. elim: k r i => /= [r i i_gt0 H rE mE| k IH r i i_gt0 H rE mE]. have /H/eqP[] : 0 < totient m < i. by rewrite totient_gt0 ?(leq_trans _ m_gt1) // -[i]mE [_ < _]totient_leq. by apply: cyclic.Euler_exp_totient. have niE : (n ^ i = r * n %[mod m])%N by rewrite rE modnMml -expnSr prednK. case: eqP => [rnE|/eqP rnE]. by rewrite niE {1}(modn_small m_gt1). apply: IH => [|i1 /andP[i1_gt0]||] //. rewrite ltnS leq_eqVlt => /orP[/eqP->|i1Li]. by rewrite niE {1}(modn_small m_gt1). by apply: H; rewrite i1_gt0. by rewrite mE addnS. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)