From 0b9c8e14a4ff66f9a9815065be9c0e98443e4336 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 4 Jun 2015 21:39:50 -0400
Subject: [PATCH] fix(*/init/nat): fix occurrences where both theorem and
 [unfold-c] were used

---
 hott/init/nat.hlean   | 8 ++++----
 library/init/nat.lean | 8 ++++----
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean
index d5b719010..bfa3a244c 100644
--- a/hott/init/nat.hlean
+++ b/hott/init/nat.hlean
@@ -73,16 +73,16 @@ namespace nat
 
   theorem le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H
 
-  theorem succ_le_succ [unfold-c 3] {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
+  definition succ_le_succ [unfold-c 3] {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
   by induction H;reflexivity;exact le.step v_0
 
-  theorem pred_le_pred [unfold-c 3] {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
+  definition pred_le_pred [unfold-c 3] {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
   by induction H;reflexivity;cases b;exact v_0;exact le.step v_0
 
-  theorem le_of_succ_le_succ [unfold-c 3] {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m :=
+  definition le_of_succ_le_succ [unfold-c 3] {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m :=
   pred_le_pred H
 
-  theorem le_succ_of_pred_le [unfold-c 1] {n m : ℕ} (H : pred n ≤ m) : n ≤ succ m :=
+  definition le_succ_of_pred_le [unfold-c 1] {n m : ℕ} (H : pred n ≤ m) : n ≤ succ m :=
   by cases n;exact le.step H;exact succ_le_succ H
 
   theorem not_succ_le_self {n : ℕ} : ¬succ n ≤ n :=
diff --git a/library/init/nat.lean b/library/init/nat.lean
index 83cec94fa..2bc07fa85 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -73,16 +73,16 @@ namespace nat
 
   theorem le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H
 
-  theorem succ_le_succ [unfold-c 3] {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
+  theorem succ_le_succ {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
   by induction H;reflexivity;exact le.step v_0
 
-  theorem pred_le_pred [unfold-c 3] {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
+  theorem pred_le_pred {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
   by induction H;reflexivity;cases b;exact v_0;exact le.step v_0
 
-  theorem le_of_succ_le_succ [unfold-c 3] {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m :=
+  theorem le_of_succ_le_succ {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m :=
   pred_le_pred H
 
-  theorem le_succ_of_pred_le [unfold-c 1] {n m : ℕ} (H : pred n ≤ m) : n ≤ succ m :=
+  theorem le_succ_of_pred_le {n m : ℕ} (H : pred n ≤ m) : n ≤ succ m :=
   by cases n;exact le.step H;exact succ_le_succ H
 
   theorem not_succ_le_self {n : ℕ} : ¬succ n ≤ n :=