diff options
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 |