diff options
Diffstat (limited to 'theories/QArith')
| -rw-r--r-- | theories/QArith/QArith_base.v | 4 | ||||
| -rw-r--r-- | theories/QArith/Qcanon.v | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 75bd9c5e6..5199333ed 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -79,9 +79,9 @@ Qed. Lemma Qge_alt : forall p q, (p>=q) <-> (p?=q <> Lt). Proof. unfold Qle, Qcompare, Zle. -split; intros; swap H. +split; intros; contradict H. rewrite Zcompare_Gt_Lt_antisym; auto. -rewrite Zcompare_Gt_Lt_antisym in H0; auto. +rewrite Zcompare_Gt_Lt_antisym in H; auto. Qed. Hint Unfold Qeq Qlt Qle: qarith. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index cfe0187a3..06d653e30 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -139,7 +139,7 @@ Theorem Qc_eq_dec : forall x y:Qc, {x=y} + {x<>y}. Proof. intros. destruct (Qeq_dec x y) as [H|H]; auto. - right; swap H; subst; auto with qarith. + right; contradict H; subst; auto with qarith. Defined. (** The addition, multiplication and opposite are defined |