proposition: Lemma poly_order_eq0_rmodp (R : ringType) (h p : {poly R}) m n : poly_order h p n = 0%N -> 0 < m <= n -> rmodp (p^+ m) h != 1.
proof: Proof. rewrite -[_ <= n]ltnS /poly_order; case: pickP => // HM _ /andP[m_gt0 mLn]. by have /= := HM (Ordinal mLn); case: (m) m_gt0 => //= k _ /idP/negP. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)