proposition: Lemma exp_incr_expp R (x : R) (H1x : 1 <= x) (m n : nat) : (m <= n)%N -> x ^+ m <= x ^+ n.
proof: Proof. move/subnK => <-; rewrite exprD. exact/ler_peMl/exprn_ege1/H1x/exprn_ge0/le_trans/H1x. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) mathcomp(bigenough)