proposition: Lemma leR_wiexpR2l x : 0 <= x -> x <= 1 -> {homo (pow x) : m n / (n <= m)%nat >-> m <= n}.
proof: Proof. move/RleP; rewrite le0r => /orP[/eqP -> _ m n|/RltP x0 x1 m n /leP nm]. case: n => [|n nm]. case: m => [_ |m _]. by apply/RleP; rewrite Order.POrderTheory.lexx. by rewrite pow_ne_zero. rewrite pow_ne_zero; last by case: m nm. rewrite pow_ne_zero //. by apply/RleP; rewrite Order.POrderTheory.lexx. apply invR_le => //. - exact/expR_gt0. - exact/expR_gt0. - rewrite -expRV; last exact/gtR_eqF. rewrite -expRV; last exact/gtR_eqF. apply Rle_pow => //. by rewrite -invR1; apply leR_inv => //; exact/ltRP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)