From 64d2cc60c2118e546fbc7a69b7cc9dcde468b900 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 7 Nov 2014 10:46:44 -0800
Subject: [PATCH] feat(library/data/nat/wf): add nat.lt is well founded theorem

---
 library/data/nat/default.lean |  2 +-
 library/data/nat/wf.lean      | 17 +++++++++++++++++
 2 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 library/data/nat/wf.lean

diff --git a/library/data/nat/default.lean b/library/data/nat/default.lean
index 89b96899f..49532ac6f 100644
--- a/library/data/nat/default.lean
+++ b/library/data/nat/default.lean
@@ -2,4 +2,4 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Jeremy Avigad
 
-import .basic .order .sub .div
+import .basic .order .sub .div .wf
diff --git a/library/data/nat/wf.lean b/library/data/nat/wf.lean
new file mode 100644
index 000000000..2649922d5
--- /dev/null
+++ b/library/data/nat/wf.lean
@@ -0,0 +1,17 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+import data.nat.order logic.wf
+open nat eq.ops
+
+theorem lt.wf [instance] : well_founded lt :=
+well_founded.intro
+ (take n, nat.induction_on n
+    (acc.intro zero (λ (y : nat) (H : y < 0),
+      absurd H !not_lt_zero))
+    (λ (n : nat) (iH : acc lt n),
+      acc.intro (succ n) (λ (m : nat) (H : m < succ n),
+        have H₁ : m < n ∨ m = n, from le_imp_lt_or_eq (succ_le_cancel (lt_imp_le_succ H)),
+        or.elim H₁
+          (assume Hlt : m < n, acc.inv iH Hlt)
+          (assume Heq : m = n, Heq⁻¹ ▸ iH))))