From 7dc055cfc9637fde80de6eba8cbc478df3155c22 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 30 Nov 2014 15:10:10 -0800
Subject: [PATCH] chore(library/data/nat/decl): remove leftover

---
 library/data/nat/decl.lean | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/library/data/nat/decl.lean b/library/data/nat/decl.lean
index 6d1bdd2c1..c203c1ac7 100644
--- a/library/data/nat/decl.lean
+++ b/library/data/nat/decl.lean
@@ -147,10 +147,6 @@ namespace nat
   definition le.is_decidable_rel [instance] : decidable_rel le :=
   λ a b, decidable_iff_equiv _ (iff.intro le.of_eq_or_lt eq_or_lt_of_le)
 
-  inductive le2 (a : nat) : nat → Prop :=
-  refl    : le2 a a,
-  of_lt : ∀ {b}, lt a b → le2 a b
-
   definition le.rec_on {a : nat} {P : nat → Prop} {b : nat} (H : a ≤ b) (H₁ : P a) (H₂ : ∀ b, a < b → P b) : P b :=
   begin
     cases H with (b', hlt),