diff options
Diffstat (limited to 'theories/QArith/Qreals.v')
| -rw-r--r-- | theories/QArith/Qreals.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 20b5cb236b..5a23a20811 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -19,6 +19,7 @@ intros. now apply not_O_IZR. Qed. +#[global] Hint Resolve IZR_nz Rmult_integral_contrapositive : core. Lemma eqR_Qeq : forall x y : Q, Q2R x = Q2R y -> x==y. |