diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-04-07 13:53:25 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-04-07 13:53:25 +0200 |
| commit | 0cd64f60b1057e4c3daa0523ed42b00c315cf136 (patch) | |
| tree | 4cacd9de3b3a89f4e3b152fe22492f81557ec3e2 /theories/Reals/RIneq.v | |
| parent | fee2365f13900b4d4f4b88c986cbbf94403eeefa (diff) | |
Add some hints to the "real" database to automatically discharge literal comparisons.
Diffstat (limited to 'theories/Reals/RIneq.v')
| -rw-r--r-- | theories/Reals/RIneq.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 7e1cc3e03..711703ad7 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1926,6 +1926,17 @@ Proof. omega. Qed. +Lemma IZR_neq : forall z1 z2:Z, z1 <> z2 -> IZR z1 <> IZR z2. +Proof. +intros; red; intro; elim H; apply eq_IZR; assumption. +Qed. + +Hint Extern 0 (IZR _ <= IZR _) => apply IZR_le, Zle_bool_imp_le, eq_refl : real. +Hint Extern 0 (IZR _ >= IZR _) => apply Rle_ge, IZR_le, Zle_bool_imp_le, eq_refl : real. +Hint Extern 0 (IZR _ < IZR _) => apply IZR_lt, eq_refl : real. +Hint Extern 0 (IZR _ > IZR _) => apply IZR_lt, eq_refl : real. +Hint Extern 0 (IZR _ <> IZR _) => apply IZR_neq, Zeq_bool_neq, eq_refl : real. + Lemma one_IZR_lt1 : forall n:Z, -1 < IZR n < 1 -> n = 0%Z. Proof. intros z [H1 H2]. |