proposition: Lemma poly_order_leq (R : ringType) (h p : {poly R}) n : 0 < n -> poly_order h p n <= n.
proof: Proof. by rewrite /poly_order; case: pickP => // x Hx; case: arg_minnP => // [] [[|m]]. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)