From b45ffd0bc0904e3d3325724e99b94239f5153b64 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 19 Feb 2021 16:13:45 +0100
Subject: Terminate some lemmas with Qed.

Since the proofs start by applying or destructuring Qed-ed lemmas, they cannot
be used in a computational setting, so no need for them to be Defined.
---
 theories/Reals/Abstract/ConstructiveReals.v          | 4 ++--
 theories/Reals/Abstract/ConstructiveRealsMorphisms.v | 2 +-
 theories/Reals/Cauchy/ConstructiveCauchyReals.v      | 3 ---
 theories/Reals/Cauchy/ConstructiveRcomplete.v        | 4 ++--
 4 files changed, 5 insertions(+), 8 deletions(-)

diff --git a/theories/Reals/Abstract/ConstructiveReals.v b/theories/Reals/Abstract/ConstructiveReals.v
index 60fad8795a..5a599587d0 100644
--- a/theories/Reals/Abstract/ConstructiveReals.v
+++ b/theories/Reals/Abstract/ConstructiveReals.v
@@ -285,14 +285,14 @@ Lemma CRlt_trans : forall {R : ConstructiveReals} (x y z : CRcarrier R),
 Proof.
   intros. apply (CRlt_le_trans _ y _ H).
   apply CRlt_asym. exact H0.
-Defined.
+Qed.
 
 Lemma CRlt_trans_flip : forall {R : ConstructiveReals} (x y z : CRcarrier R),
     y < z -> x < y -> x < z.
 Proof.
   intros. apply (CRlt_le_trans _ y). exact H0.
   apply CRlt_asym. exact H.
-Defined.
+Qed.
 
 Lemma CReq_refl : forall {R : ConstructiveReals} (x : CRcarrier R),
     x == x.
diff --git a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v
index 53b5aca38c..6ed5845440 100644
--- a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v
+++ b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v
@@ -232,7 +232,7 @@ Proof.
   apply CRplus_lt_compat_l.
   apply (CRle_lt_trans _ (CR_of_Q R 0)). apply CRle_refl.
   apply CR_of_Q_lt. exact H.
-Defined.
+Qed.
 
 Lemma CRplus_neg_rat_lt : forall {R : ConstructiveReals} (x : CRcarrier R) (q : Q),
     Qlt q 0 -> CRlt R (CRplus R x (CR_of_Q R q)) x.
diff --git a/theories/Reals/Cauchy/ConstructiveCauchyReals.v b/theories/Reals/Cauchy/ConstructiveCauchyReals.v
index 8a11c155ce..4fb3846abc 100644
--- a/theories/Reals/Cauchy/ConstructiveCauchyReals.v
+++ b/theories/Reals/Cauchy/ConstructiveCauchyReals.v
@@ -320,7 +320,6 @@ Proof.
   - contradiction.
   - exact Hxltz.
 Qed.
-(* Todo: this was Defined. Why *)
 
 Lemma CReal_lt_le_trans : forall x y z : CReal,
     x < y -> y <= z -> x < z.
@@ -330,7 +329,6 @@ Proof.
   - exact Hxltz.
   - contradiction.
 Qed.
-(* Todo: this was Defined. Why *)
 
 Lemma CReal_le_trans : forall x y z : CReal,
     x <= y -> y <= z -> x <= z.
@@ -347,7 +345,6 @@ Proof.
   apply (CReal_lt_le_trans _ y _ Hxlty).
   apply CRealLt_asym; exact Hyltz.
 Qed.
-(* Todo: this was Defined. Why *)
 
 Lemma CRealEq_trans : forall x y z : CReal,
     CRealEq x y -> CRealEq y z -> CRealEq x z.
diff --git a/theories/Reals/Cauchy/ConstructiveRcomplete.v b/theories/Reals/Cauchy/ConstructiveRcomplete.v
index 70d2861d17..38eb9df0ea 100644
--- a/theories/Reals/Cauchy/ConstructiveRcomplete.v
+++ b/theories/Reals/Cauchy/ConstructiveRcomplete.v
@@ -75,7 +75,7 @@ Proof.
     rewrite inject_Q_plus, (opp_inject_Q 2).
     ring_simplify. exact H.
     rewrite Qinv_plus_distr. reflexivity.
-Defined.
+Qed.
 
 (* ToDo: Move to ConstructiveCauchyAbs.v *)
 Lemma Qabs_Rabs : forall q : Q,
@@ -688,7 +688,7 @@ Proof.
   exact (a i j H0 H1).
   exists l. intros p. destruct (cv p).
   exists x. exact c.
-Defined.
+Qed.
 
 (* ToDO: Belongs into sumbool.v *)
 Section connectives.
-- 
cgit v1.2.3