proposition: Lemma poly_order_gt0_rmodp (R : ringType) (h p : {poly R}) n : 0 < poly_order h p n -> rmodp (p^+ poly_order h p n) h == 1.
proof: Proof. by rewrite /poly_order; case: pickP => // x Hx _; case: arg_minnP. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)