diff options
| author | Vincent Semeria | 2020-03-30 18:13:37 +0200 |
|---|---|---|
| committer | Vincent Semeria | 2020-03-30 18:13:37 +0200 |
| commit | ea0bfc872a1363b47bf91e65fba0ecb770b39981 (patch) | |
| tree | 4497de351546392ca7d1e7dfa78e606221c15adc | |
| parent | ba8783c42ad3e2b22d917336ce5e52245d09441b (diff) | |
Missing apartness notations
| -rw-r--r-- | theories/Reals/Abstract/ConstructiveAbs.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Reals/Abstract/ConstructiveAbs.v b/theories/Reals/Abstract/ConstructiveAbs.v index a98cd7d44a..d357ad2d54 100644 --- a/theories/Reals/Abstract/ConstructiveAbs.v +++ b/theories/Reals/Abstract/ConstructiveAbs.v @@ -198,7 +198,7 @@ Proof. Qed. Lemma CRabs_appart_0 : forall {R : ConstructiveReals} (x : CRcarrier R), - 0 < CRabs R x -> CRapart R x 0. + 0 < CRabs R x -> x ≶ 0. Proof. intros. destruct (CRltLinear R). clear p. pose proof (s _ x _ H) as [pos|neg]. @@ -224,8 +224,8 @@ Lemma CRabs_mult : forall {R : ConstructiveReals} (x y : CRcarrier R), Proof. intro R. assert (forall (x y : CRcarrier R), - CRapart R x 0 - -> CRapart R y 0 + x ≶ 0 + -> y ≶ 0 -> CRabs R (x * y) == CRabs R x * CRabs R y) as prep. { intros. destruct H, H0. + rewrite CRabs_right, CRabs_left, CRabs_left. |