Remove the <8.16 compatibility lemmas

LM/R_compl.v

@@ -21,57 +21,6 @@ From Coquelicot Require Export Coquelicot.
 
 Open Scope R_scope.
 
-(* pris de la lib std en attendant 8.16 pour tout le monde *)
-
-Lemma Rinv_1 : / 1 = 1.
-Proof.
-  field.
-Qed.
-
-Lemma Rinv_0 : / 0 = 0.
-Proof.
-rewrite RinvImpl.Rinv_def.
-case Req_appart_dec.
-- easy.
-- intros [H|H] ; elim Rlt_irrefl with (1 := H).
-Qed.
-
-Lemma Rinv_inv r : / / r = r.
-Proof.
-destruct (Req_dec r 0) as [->|H].
-- rewrite Rinv_0.
-  apply Rinv_0.
-- now field.
-Qed.
-
-Lemma Rinv_mult r1 r2 : / (r1 * r2) = / r1 * / r2.
-Proof.
-destruct (Req_dec r1 0) as [->|H1].
-- rewrite Rinv_0, 2!Rmult_0_l.
-  apply Rinv_0.
-- destruct (Req_dec r2 0) as [->|H2].
-  + rewrite Rinv_0, 2!Rmult_0_r.
-    apply Rinv_0.
-  + now field.
-Qed.
-
-Lemma pow_inv x n : (/ x) ^ n = / x ^ n.
-Proof.
-induction n as [|n IH] ; simpl.
-- apply eq_sym, Rinv_1.
-- rewrite Rinv_mult.
-  now apply f_equal.
-Qed.
-
-Lemma Rsqr_div' x y : Rsqr (x / y) = Rsqr x / Rsqr y.
-Proof.
-  unfold Rsqr, Rdiv.
-  rewrite Rinv_mult.
-  ring.
-Qed.
-
-(* fin des lemmes pris de 8.16 *)
-
 Section RC. (* TODO: découper cette section *)
 
 Lemma Runbounded (y : R) : exists (x : R), x > y.

Lebesgue/R_compl.v

@@ -22,56 +22,6 @@ From Lebesgue Require Import logic_compl.
 
 Section R_ring_compl.
 
-(* pris de la lib std en attendant 8.16 pour tout le monde *)
-
-Lemma Rinv_1 : / 1 = 1.
-Proof.
-  field.
-Qed.
-
-Lemma Rinv_0 : / 0 = 0.
-Proof.
-rewrite RinvImpl.Rinv_def.
-case Req_appart_dec.
-- easy.
-- intros [H|H] ; elim Rlt_irrefl with (1 := H).
-Qed.
-
-Lemma Rinv_inv r : / / r = r.
-Proof.
-destruct (Req_dec r 0) as [->|H].
-- rewrite Rinv_0.
-  apply Rinv_0.
-- now field.
-Qed.
-
-Lemma Rinv_mult r1 r2 : / (r1 * r2) = / r1 * / r2.
-Proof.
-destruct (Req_dec r1 0) as [->|H1].
-- rewrite Rinv_0, 2!Rmult_0_l.
-  apply Rinv_0.
-- destruct (Req_dec r2 0) as [->|H2].
-  + rewrite Rinv_0, 2!Rmult_0_r.
-    apply Rinv_0.
-  + now field.
-Qed.
-
-Lemma pow_inv x n : (/ x)^n = / x^n.
-Proof.
-induction n as [|n IH] ; simpl.
-- apply eq_sym, Rinv_1.
-- rewrite Rinv_mult.
-  now apply f_equal.
-Qed.
-
-Lemma Rsqr_div' x y : Rsqr (x / y) = Rsqr x / Rsqr y.
-Proof.
-  unfold Rsqr, Rdiv.
-  rewrite Rinv_mult.
-  ring.
-Qed.
-
-(* fin des lemmes pris de 8.16 *)
 (** Complements on ring operations Rplus and Rmult. **)
 
 Lemma Rplus_not_eq_compat_l : forall r r1 r2, r1 <> r2 -> r + r1 <> r + r2.