proposition: Lemma poly_orderE (R : ringType) (h p : {poly R}) n m : 0 < m <= n -> rmodp (p ^+ m) h = 1 -> (forall k, 0 < k -> rmodp (p^+ k) h = 1 -> m <= k) -> poly_order h p n = m.
proof: Proof. move=> /andP[m_gt0 mLn] /eqP mM HmM. rewrite -ltnS in mLn. rewrite /poly_order; case: pickP => [z zM|/(_ (Ordinal mLn))]; last first. by rewrite prednK //= (eqP mM) eqxx. case: arg_minnP => //. move=> i /eqP /HmM /= Hj /(_ (Ordinal mLn)). rewrite prednK //= => /(_ mM) iLm. apply/eqP; rewrite eqn_leq Hj // andbT. by case: (i: nat) iLm. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)