diff options
| author | Guillaume Melquiond | 2021-02-19 16:13:45 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-02-19 16:28:35 +0100 |
| commit | b45ffd0bc0904e3d3325724e99b94239f5153b64 (patch) | |
| tree | 1c588c78469bfb5bc8d9aeeae537389f353e85c8 /theories/Reals/Abstract | |
| parent | a2938972537389b9813794147412f51494f48dd1 (diff) | |
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.
Diffstat (limited to 'theories/Reals/Abstract')
| -rw-r--r-- | theories/Reals/Abstract/ConstructiveReals.v | 4 | ||||
| -rw-r--r-- | theories/Reals/Abstract/ConstructiveRealsMorphisms.v | 2 |
2 files changed, 3 insertions, 3 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. |