proposition: Lemma poly_order_lt (R : ringType) (h p : {poly R}) m n : 0 < m < poly_order h p n -> rmodp (p^+ m) h != 1.
proof: Proof. rewrite /poly_order; case: pickP=> [x Hx|]; last by rewrite ltn0 andbF. case: arg_minnP => // i Hi Hmin /andP[m_gt0 mLi]. have mLn : m < n.+1. by rewrite (leq_trans mLi) // (leq_trans _ (ltn_ord i)) //; case: (i : nat). apply/negP; rewrite -[m]prednK // => /(Hmin (Ordinal mLn)) /=. rewrite leqNgt; case: (i : nat) mLi => [/=|j ->//]. by case: (m) m_gt0. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)