diff --git a/hott/algebra/order.hlean b/hott/algebra/order.hlean
index c16a48286..acebf3616 100644
--- a/hott/algebra/order.hlean
+++ b/hott/algebra/order.hlean
@@ -23,24 +23,24 @@ section
   variable [s : weak_order A]
   include s
 
-  theorem le.refl (a : A) : a ≤ a := !weak_order.le_refl
+  definition le.refl (a : A) : a ≤ a := !weak_order.le_refl
 
-  theorem le_of_eq {a b : A} (H : a = b) : a ≤ b := H ▸ le.refl a
+  definition le_of_eq {a b : A} (H : a = b) : a ≤ b := H ▸ le.refl a
 
-  theorem le.trans [trans] {a b c : A} : a ≤ b → b ≤ c → a ≤ c := !weak_order.le_trans
+  definition le.trans [trans] {a b c : A} : a ≤ b → b ≤ c → a ≤ c := !weak_order.le_trans
 
-  theorem ge.trans [trans] {a b c : A} (H1 : a ≥ b) (H2: b ≥ c) : a ≥ c := le.trans H2 H1
+  definition ge.trans [trans] {a b c : A} (H1 : a ≥ b) (H2: b ≥ c) : a ≥ c := le.trans H2 H1
 
-  theorem le.antisymm {a b : A} : a ≤ b → b ≤ a → a = b := !weak_order.le_antisymm
+  definition le.antisymm {a b : A} : a ≤ b → b ≤ a → a = b := !weak_order.le_antisymm
 
   -- Alternate syntax. (Abbreviations do not migrate well.)
-  theorem eq_of_le_of_ge {a b : A} : a ≤ b → b ≤ a → a = b := !le.antisymm
+  definition eq_of_le_of_ge {a b : A} : a ≤ b → b ≤ a → a = b := !le.antisymm
 end
 
 structure linear_weak_order [class] (A : Type) extends weak_order A :=
 (le_total : Πa b, le a b ⊎ le b a)
 
-theorem le.total [s : linear_weak_order A] (a b : A) : a ≤ b ⊎ b ≤ a :=
+definition le.total [s : linear_weak_order A] (a b : A) : a ≤ b ⊎ b ≤ a :=
 !linear_weak_order.le_total
 
 /- strict orders -/
@@ -53,15 +53,15 @@ section
   variable [s : strict_order A]
   include s
 
-  theorem lt.irrefl (a : A) : ¬ a < a := !strict_order.lt_irrefl
-  theorem not_lt_self (a : A) : ¬ a < a := !lt.irrefl   -- alternate syntax
+  definition lt.irrefl (a : A) : ¬ a < a := !strict_order.lt_irrefl
+  definition not_lt_self (a : A) : ¬ a < a := !lt.irrefl   -- alternate syntax
 
   theorem lt_self_iff_empty (a : A) : a < a ↔ empty :=
   iff_empty_intro (lt.irrefl a)
 
-  theorem lt.trans [trans] {a b c : A} : a < b → b < c → a < c := !strict_order.lt_trans
+  definition lt.trans [trans] {a b c : A} : a < b → b < c → a < c := !strict_order.lt_trans
 
-  theorem gt.trans [trans] {a b c : A} (H1 : a > b) (H2: b > c) : a > c := lt.trans H2 H1
+  definition gt.trans [trans] {a b c : A} (H1 : a > b) (H2: b > c) : a > c := lt.trans H2 H1
 
   theorem ne_of_lt {a b : A} (lt_ab : a < b) : a ≠ b :=
   assume eq_ab : a = b,
@@ -98,13 +98,13 @@ section
   variables {a b c : A}
   include s
 
-  theorem le_of_lt : a < b → a ≤ b := !order_pair.le_of_lt
+  definition le_of_lt : a < b → a ≤ b := !order_pair.le_of_lt
 
-  theorem lt_of_lt_of_le [trans] : a < b → b ≤ c → a < c := !order_pair.lt_of_lt_of_le
+  definition lt_of_lt_of_le [trans] : a < b → b ≤ c → a < c := !order_pair.lt_of_lt_of_le
 
-  theorem lt_of_le_of_lt [trans] : a ≤ b → b < c → a < c := !order_pair.lt_of_le_of_lt
+  definition lt_of_le_of_lt [trans] : a ≤ b → b < c → a < c := !order_pair.lt_of_le_of_lt
 
-  private theorem lt_irrefl (s' : order_pair A) (a : A) : ¬ a < a := !order_pair.lt_irrefl
+  private definition lt_irrefl (s' : order_pair A) (a : A) : ¬ a < a := !order_pair.lt_irrefl
 
   private theorem lt_trans (s' : order_pair A) (a b c: A) (lt_ab : a < b) (lt_bc : b < c) : a < c :=
     lt_of_lt_of_le lt_ab (le_of_lt lt_bc)
@@ -112,9 +112,9 @@ section
   definition order_pair.to_strict_order [trans_instance] [reducible] : strict_order A :=
   ⦃ strict_order, s, lt_irrefl := lt_irrefl s, lt_trans := lt_trans s ⦄
 
-  theorem gt_of_gt_of_ge [trans] (H1 : a > b) (H2 : b ≥ c) : a > c := lt_of_le_of_lt H2 H1
+  definition gt_of_gt_of_ge [trans] (H1 : a > b) (H2 : b ≥ c) : a > c := lt_of_le_of_lt H2 H1
 
-  theorem gt_of_ge_of_gt [trans] (H1 : a ≥ b) (H2 : b > c) : a > c := lt_of_lt_of_le H2 H1
+  definition gt_of_ge_of_gt [trans] (H1 : a ≥ b) (H2 : b > c) : a > c := lt_of_lt_of_le H2 H1
 
   theorem not_le_of_gt (H : a > b) : ¬ a ≤ b :=
   assume H1 : a ≤ b,
@@ -129,7 +129,7 @@ structure strong_order_pair [class] (A : Type) extends weak_order A, has_lt A :=
 (le_iff_lt_sum_eq : Πa b, le a b ↔ lt a b ⊎ a = b)
 (lt_irrefl : Π a, ¬ lt a a)
 
-theorem le_iff_lt_sum_eq [s : strong_order_pair A] {a b : A} : a ≤ b ↔ a < b ⊎ a = b :=
+definition le_iff_lt_sum_eq [s : strong_order_pair A] {a b : A} : a ≤ b ↔ a < b ⊎ a = b :=
 !strong_order_pair.le_iff_lt_sum_eq
 
 theorem lt_sum_eq_of_le [s : strong_order_pair A] {a b : A} (le_ab : a ≤ b) : a < b ⊎ a = b :=
@@ -138,7 +138,7 @@ iff.mp le_iff_lt_sum_eq le_ab
 theorem le_of_lt_sum_eq [s : strong_order_pair A] {a b : A} (lt_sum_eq : a < b ⊎ a = b) : a ≤ b :=
 iff.mpr le_iff_lt_sum_eq lt_sum_eq
 
-private theorem lt_irrefl' [s : strong_order_pair A] (a : A) : ¬ a < a :=
+private definition lt_irrefl' [s : strong_order_pair A] (a : A) : ¬ a < a :=
 !strong_order_pair.lt_irrefl
 
 private theorem le_of_lt' [s : strong_order_pair A] (a b : A) : a < b → a ≤ b :=
diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean
index c0c990424..497a17979 100644
--- a/hott/init/nat.hlean
+++ b/hott/init/nat.hlean
@@ -43,7 +43,7 @@ namespace nat
 
   definition nat_has_le [instance] [reducible] [priority nat.prio]: has_le nat := has_le.mk nat.le
 
-  protected lemma le_refl [refl] : Π a : nat, a ≤ a :=
+  protected definition le_refl [refl] : Π a : nat, a ≤ a :=
   le.nat_refl
 
   protected definition lt [reducible] (n m : ℕ) := succ n ≤ m
@@ -83,28 +83,28 @@ namespace nat
 
   /- properties of inequality -/
 
-  protected theorem le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := p ▸ !nat.le_refl
+  protected definition le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := p ▸ !nat.le_refl
 
-  theorem le_succ (n : ℕ) : n ≤ succ n := le.step !nat.le_refl
+  definition le_succ (n : ℕ) : n ≤ succ n := le.step !nat.le_refl
 
-  theorem pred_le (n : ℕ) : pred n ≤ n := by cases n;repeat constructor
+  definition pred_le (n : ℕ) : pred n ≤ n := by cases n;repeat constructor
 
-  theorem le_succ_iff_unit [simp] (n : ℕ) : n ≤ succ n ↔ unit :=
+  definition le_succ_iff_unit [simp] (n : ℕ) : n ≤ succ n ↔ unit :=
   iff_unit_intro (le_succ n)
 
-  theorem pred_le_iff_unit [simp] (n : ℕ) : pred n ≤ n ↔ unit :=
+  definition pred_le_iff_unit [simp] (n : ℕ) : pred n ≤ n ↔ unit :=
   iff_unit_intro (pred_le n)
 
-  protected theorem le_trans {n m k : ℕ} (H1 : n ≤ m) : m ≤ k → n ≤ k :=
+  protected definition le_trans {n m k : ℕ} (H1 : n ≤ m) : m ≤ k → n ≤ k :=
   le.rec H1 (λp H2, le.step)
 
-  theorem le_succ_of_le {n m : ℕ} (H : n ≤ m) : n ≤ succ m := nat.le_trans H !le_succ
+  definition le_succ_of_le {n m : ℕ} (H : n ≤ m) : n ≤ succ m := nat.le_trans H !le_succ
 
-  theorem le_of_succ_le {n m : ℕ} (H : succ n ≤ m) : n ≤ m := nat.le_trans !le_succ H
+  definition le_of_succ_le {n m : ℕ} (H : succ n ≤ m) : n ≤ m := nat.le_trans !le_succ H
 
-  protected theorem le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H
+  protected definition le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H
 
-  theorem succ_le_succ {n m : ℕ} : n ≤ m → succ n ≤ succ m :=
+  definition succ_le_succ {n m : ℕ} : n ≤ m → succ n ≤ succ m :=
   le.rec !nat.le_refl (λa b, le.step)
 
   theorem pred_le_pred {n m : ℕ} : n ≤ m → pred n ≤ pred m :=
@@ -128,7 +128,7 @@ namespace nat
   theorem succ_le_self_iff_empty [simp] (n : ℕ) : succ n ≤ n ↔ empty :=
   iff_empty_intro not_succ_le_self
 
-  theorem zero_le : Π (n : ℕ), 0 ≤ n :=
+  definition zero_le : Π (n : ℕ), 0 ≤ n :=
   nat.rec !nat.le_refl (λa, le.step)
 
   theorem zero_le_iff_unit [simp] (n : ℕ) : 0 ≤ n ↔ unit :=