- Adjusted definitions and lemmas for asin and acos to what has been discussed

- Added derivative for asin and acos
- Added a few additional trigonometry lemmas
- Added Lemmas for the derivative of a decreasing inverse function
- Did some cleanup (move lemmas to the files where they belong)

4 files changed, 16 insertions, 2 deletions

diff --git a/doc/changelog/10-standard-library/00000-title.rst b/doc/changelog/10-standard-library/00000-title.rst
index a182366f03..d517a0e709 100644
--- a/doc/changelog/10-standard-library/00000-title.rst
+++ b/doc/changelog/10-standard-library/00000-title.rst
@@ -1,2 +1,3 @@
 
 **Standard library**
+
diff --git a/doc/changelog/10-standard-library/09803-trigo.rst b/doc/changelog/10-standard-library/09803-trigo.rst
deleted file mode 100644
index 10cb069a4c..0000000000
--- a/doc/changelog/10-standard-library/09803-trigo.rst
+++ /dev/null
@@ -1,2 +0,0 @@
-
-- Addition to the Reals theory (`#09803 <https://github.com/coq/coq/pull/09803>`_ by Laurent Théry):
diff --git a/doc/changelog/10-standard-library/9803-reals.rst b/doc/changelog/10-standard-library/9803-reals.rst
new file mode 100644
index 0000000000..86c5e45bc1
--- /dev/null
+++ b/doc/changelog/10-standard-library/9803-reals.rst
@@ -0,0 +1,14 @@
+- **Changed:**
+  Cleanup of names in the Reals theory: replaced `tan_is_inj` with `tan_inj` and replaced `atan_right_inv` with `tan_atan` -
+  compatibility notations are provided. Moved various auxiliary lemmas from `Ratan.v` to more appropriate places.
+  (`#9803 <https://github.com/coq/coq/pull/9803>`_,
+  by Laurent Théry and Michael Soegtrop).
+
+- **Added:** to the Reals theory:
+  inverse trigonometric functions `asin` and `acos` with lemmas for the derivatives, bounds and special values of these functions;
+  an extensive set of identities between trigonometric functions and their inverse functions;
+  lemmas for the injectivity of sine and cosine;
+  lemmas on the derivative of the inverse of decreasing functions and on the derivative of horizontally mirrored functions;
+  various generic auxiliary lemmas and definitions for Rsqr, sqrt, posreal an others.
+  (`#9803 <https://github.com/coq/coq/pull/9803>`_,
+  by Laurent Théry and Michael Soegtrop).
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index e64b4be454..7fa621c11c 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -558,6 +558,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Reals/Rtrigo_fun.v
     theories/Reals/Rtrigo1.v
     theories/Reals/Rtrigo.v
+    theories/Reals/Rtrigo_facts.v
     theories/Reals/Ratan.v
     theories/Reals/Machin.v
     theories/Reals/SplitAbsolu.v