blob: 27d89b2f8beda6526608807a9937f95d9eaa36c3 (
plain)
1
2
3
4
5
6
7
8
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
).
|
