diff options
| -rw-r--r-- | theories/QArith/QArith_base.v | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 2c80aff40c..16733c3b8c 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -157,16 +157,15 @@ Qed. (** We now consider [Q] seen as a setoid. *) -Definition Q_Setoid : Setoid_Theory Q Qeq. -Proof. - split; red; unfold Qeq in |- *; auto; apply Qeq_trans. -Qed. - -Add Setoid Q Qeq Q_Setoid as Qsetoid. - -Hint Resolve (Seq_refl Q Qeq Q_Setoid): qarith. -Hint Resolve (Seq_sym Q Qeq Q_Setoid): qarith. -Hint Resolve (Seq_trans Q Qeq Q_Setoid): qarith. +Add Relation Q Qeq + reflexivity proved by Qeq_refl + symmetry proved by Qeq_sym + transitivity proved by Qeq_trans +as Q_Setoid. + +Hint Resolve Qeq_refl : qarith. +Hint Resolve Qeq_sym : qarith. +Hint Resolve Qeq_trans : qarith. Theorem Qnot_eq_sym : forall x y, ~x == y -> ~y == x. Proof. |