From 5ca37dace0fab99dd2f57788ae9b1746f291e21c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 9 Aug 2015 20:47:41 -0700
Subject: [PATCH] fix(library/data/nat/order): fixes #786

---
 library/data/nat/order.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index e0ea11154..85595c613 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -298,7 +298,7 @@ assume Plt, lt.trans Plt (self_lt_succ j)
 /- other forms of induction -/
 
 protected definition strong_rec_on {P : nat → Type} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n :=
-nat.rec (λm, not.elim !not_lt_zero)
+nat.rec (λm h, absurd h !not_lt_zero)
   (λn' (IH : ∀ {m : ℕ}, m < n' → P m) m l,
      or.by_cases (lt_or_eq_of_le (le_of_lt_succ l))
     IH (λ e, eq.rec (H n' @IH) e⁻¹)) (succ n) n !lt_succ_self