diff options
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/RIneq.v | 10 | ||||
| -rw-r--r-- | theories/Reals/ROrderedType.v | 2 |
2 files changed, 7 insertions, 5 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 70f4ff0d9b..944e7da210 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -43,7 +43,7 @@ Hint Immediate Rge_refl: rorders. Lemma Rlt_irrefl : forall r, ~ r < r. Proof. - generalize Rlt_asym. intuition eauto. + intros r H; eapply Rlt_asym; eauto. Qed. Hint Resolve Rlt_irrefl: real. @@ -64,7 +64,9 @@ Qed. (**********) Lemma Rlt_dichotomy_converse : forall r1 r2, r1 < r2 \/ r1 > r2 -> r1 <> r2. Proof. - generalize Rlt_not_eq Rgt_not_eq. intuition eauto. + intuition. + - apply Rlt_not_eq in H1. eauto. + - apply Rgt_not_eq in H1. eauto. Qed. Hint Resolve Rlt_dichotomy_converse: real. @@ -74,7 +76,7 @@ Hint Resolve Rlt_dichotomy_converse: real. Lemma Req_dec : forall r1 r2, r1 = r2 \/ r1 <> r2. Proof. intros; generalize (total_order_T r1 r2) Rlt_dichotomy_converse; - intuition eauto 3. + unfold not; intuition eauto 3. Qed. Hint Resolve Req_dec: real. @@ -175,7 +177,7 @@ Proof. eauto using Rnot_gt_ge with rorders. Qed. Lemma Rlt_not_le : forall r1 r2, r2 < r1 -> ~ r1 <= r2. Proof. generalize Rlt_asym Rlt_dichotomy_converse; unfold Rle in |- *. - intuition eauto 3. + unfold not; intuition eauto 3. Qed. Hint Immediate Rlt_not_le: real. diff --git a/theories/Reals/ROrderedType.v b/theories/Reals/ROrderedType.v index 0a8d89c77f..eeafbde9b9 100644 --- a/theories/Reals/ROrderedType.v +++ b/theories/Reals/ROrderedType.v @@ -15,7 +15,7 @@ Local Open Scope R_scope. Lemma Req_dec : forall r1 r2:R, {r1 = r2} + {r1 <> r2}. Proof. intros; generalize (total_order_T r1 r2) Rlt_dichotomy_converse; - intuition eauto 3. + intuition eauto. Qed. Definition Reqb r1 r2 := if Req_dec r1 r2 then true else false. |