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/DiscrR.v | |
| parent | fee2365f13900b4d4f4b88c986cbbf94403eeefa (diff) | |
Add some hints to the "real" database to automatically discharge literal comparisons.
Diffstat (limited to 'theories/Reals/DiscrR.v')
| -rw-r--r-- | theories/Reals/DiscrR.v | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index 05911cd53..7f26c1b86 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -22,11 +22,6 @@ Proof. intros; rewrite H; reflexivity. 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. - Ltac discrR := try match goal with |