proposition: Lemma ler_pXn2r n : (0 < n)%N -> {in nneg & , {mono (@GRing.exp R)^~ n : x y / x <= y}}.
proof: Proof. case: n => // n _ x y; rewrite !qualifE /= => x_ge0 y_ge0. have [-> | nzx] := eqVneq x 0; first by rewrite exprS mul0r exprn_ge0. rewrite -subr_ge0 subrXX pmulr_lge0 ?subr_ge0 //= big_ord_recr /=. rewrite subnn expr0 mul1r /= ltr_pwDr // ?exprn_gt0 ?lt0r ?nzx //. by rewrite sumr_ge0 // => i _; rewrite mulr_ge0 ?exprn_ge0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)