Avoid functions deprecated since coq v8.16

Concerning real numbers.

Author: Columbus240

theories/Topology/RFuncContinuity.v

@@ -311,7 +311,7 @@ assert (forall x:R, -1 < x / (1 + Rabs x) < 1).
   { pose proof (Rabs_pos x). lra. }
   apply and_comm, Rabs_def2.
   unfold Rdiv.
-  rewrite Rabs_mult, Rabs_Rinv; try lra.
+  rewrite Rabs_mult, Rabs_inv; try lra.
   rewrite (Rabs_right (1 + Rabs x)); [ | now left ].
   pattern 1 at 2.
   replace 1 with ((1 + Rabs x) * / (1 + Rabs x)) by (field; lra).

theories/Topology/RationalsInReals.v

@@ -25,7 +25,7 @@ Proof.
       apply lt_0_IZR in H0.
       now apply Z.lt_gt.
     - pattern eps at 2.
-      rewrite <- Rinv_involutive; auto with real;
+      rewrite <- Rinv_inv; auto with real;
         apply Rinv_lt_contravar; auto with real;
         apply Rmult_lt_0_compat; auto with real;
         apply Rlt_trans with (/ eps); auto with real.