proposition: Lemma leR_weexpR2l x : 1 <= x -> {homo (pow x) : m n / (m <= n)%nat >-> m <= n}.
proof: Proof. by move=> x1 m n /leP nm; exact/Rle_pow. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)