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