proposition: Lemma exp_incr_expn R (x : R) (H1x : 0 < x < 1) (m n : nat) : (n <= m)%N -> x ^+ m <= x ^+ n.
proof: Proof. case/andP: H1x => lt0x ltx1 /subnK <-; rewrite exprD. exact/ler_piMl/exprn_ile1/ltW/ltx1/ltW/lt0x/exprn_ge0/ltW. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) mathcomp(bigenough)