From 380181e50acc634c18905e0671fa1609d0e58041 Mon Sep 17 00:00:00 2001
From: Alessandro Bruni <brun@itu.dk>
Date: Sat, 23 Sep 2023 12:01:15 +0200
Subject: [PATCH] Lemma gt0_ltr_powR

---
 CHANGELOG_UNRELEASED.md |  3 +++
 theories/exp.v          | 10 ++++++++++
 2 files changed, 13 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index cc6e632c59..05ac6a3733 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -70,6 +70,9 @@
 - in `measure.v`:
   + definition `ess_sup`, lemma `ess_sup_ge0`
 
+- in `exp.v`:
+  + lemma `gt0_ltr_powR`
+
 ### Changed
 
 - `mnormalize` moved from `kernel.v` to `measure.v` and generalized
diff --git a/theories/exp.v b/theories/exp.v
index b21b553f90..ad2d247f77 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -676,6 +676,16 @@ move=> /predU1P[->//|xy]; first by rewrite eqxx.
 by apply/orP; right; rewrite /powR !gt_eqF// ltr_expR ltr_pmul2l// ltr_ln.
 Qed.
 
+Lemma gt0_ltr_powR (r : R) : 0 < r ->
+  {in `[0, +oo[ &, {homo powR ^~ r : x y / x < y >-> x < y}}.
+Proof.
+move=> r0 x y; rewrite !in_itv/= !andbT !le_eqVlt => /predU1P[<-|x0].
+  move=> /predU1P[<-|y0 _]; first by rewrite ltxx//.
+  by rewrite powR0 ?(gt_eqF r0)// powR_gt0.
+move=> /predU1P[<-|y0]; first rewrite ltNge ltW//.
+by rewrite /powR !gt_eqF// ltr_expR ltr_pmul2l// ltr_ln.
+Qed.
+
 Lemma powRM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r.
 Proof.
 rewrite /powR mulf_eq0.