Merge PR #13582: Generalize exp_ineq1 and add exp_ineq1_le, which holds forall Reals.

Reviewed-by: thery

1 files changed, 9 insertions, 0 deletions

diff --git a/doc/changelog/10-standard-library/13582-exp_ineq.rst b/doc/changelog/10-standard-library/13582-exp_ineq.rst
new file mode 100644
index 0000000000..27d89b2f8b
--- /dev/null
+++ b/doc/changelog/10-standard-library/13582-exp_ineq.rst
@@ -0,0 +1,9 @@
+- **Changed:**
+  Minor Changes to Rpower:
+  Generalizes exp_ineq1 to hold for all non-zero numbers.
+  Adds exp_ineq1_le, which holds for all reals (but is a <= instead of a <).
+
+  (`#13582 <https://github.com/coq/coq/pull/13582>`_,
+  by Avi Shinnar and Barry Trager, with help from Laurent Théry
+
+).