From 0cd64f60b1057e4c3daa0523ed42b00c315cf136 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Fri, 7 Apr 2017 13:53:25 +0200
Subject: Add some hints to the "real" database to automatically discharge
 literal comparisons.

---
 theories/Reals/DiscrR.v | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'theories/Reals/DiscrR.v')

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
-- 
cgit v1.2.3