proposition: Lemma pow_monotone n (x y : R) : 0 <= x <= y -> 0 <= x ^+ n <= y ^+ n.
proof: Proof. move => /andP [xp xy]. by rewrite ler_expn2r// ?andbT ?exprn_ge0// nnegrE (le_trans _ xy). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)