diff --git a/library/standard/data/bool.lean b/library/standard/data/bool.lean
index 5198a9edb9..71dd8e3c7d 100644
--- a/library/standard/data/bool.lean
+++ b/library/standard/data/bool.lean
@@ -12,7 +12,7 @@ inductive bool : Type :=
 
 namespace bool
 
-theorem induction_on {p : bool → Prop} (b : bool) (H0 : p ff) (H1 : p tt) : p b :=
+theorem cases_on {p : bool → Prop} (b : bool) (H0 : p ff) (H1 : p tt) : p b :=
 bool_rec H0 H1 b
 
 theorem bool_inhabited [instance] : inhabited bool :=
@@ -22,7 +22,7 @@ definition cond {A : Type} (b : bool) (t e : A) :=
 bool_rec e t b
 
 theorem dichotomy (b : bool) : b = ff ∨ b = tt :=
-induction_on b (or_inl (refl ff)) (or_inr (refl tt))
+cases_on b (or_inl (refl ff)) (or_inr (refl tt))
 
 theorem cond_ff {A : Type} (t e : A) : cond ff t e = e :=
 refl (cond ff t e)
@@ -52,24 +52,24 @@ refl (bor tt a)
 infixl `||`:65 := bor
 
 theorem bor_tt_right (a : bool) : a || tt = tt :=
-induction_on a (refl (ff || tt)) (refl (tt || tt))
+cases_on a (refl (ff || tt)) (refl (tt || tt))
 
 theorem bor_ff_left (a : bool) : ff || a = a :=
-induction_on a (refl (ff || ff)) (refl (ff || tt))
+cases_on a (refl (ff || ff)) (refl (ff || tt))
 
 theorem bor_ff_right (a : bool) : a || ff = a :=
-induction_on a (refl (ff || ff)) (refl (tt || ff))
+cases_on a (refl (ff || ff)) (refl (tt || ff))
 
 theorem bor_id (a : bool) : a || a = a :=
-induction_on a (refl (ff || ff)) (refl (tt || tt))
+cases_on a (refl (ff || ff)) (refl (tt || tt))
 
 theorem bor_comm (a b : bool) : a || b = b || a :=
-induction_on a
-  (induction_on b (refl (ff || ff)) (refl (ff || tt)))
-  (induction_on b (refl (tt || ff)) (refl (tt || tt)))
+cases_on a
+  (cases_on b (refl (ff || ff)) (refl (ff || tt)))
+  (cases_on b (refl (tt || ff)) (refl (tt || tt)))
 
 theorem bor_assoc (a b c : bool) : (a || b) || c = a || (b || c) :=
-induction_on a
+cases_on a
   (calc (ff || b) || c = b || c         : {bor_ff_left b}
                  ...   = ff || (b || c) : bor_ff_left (b || c)⁻¹)
   (calc (tt || b) || c = tt || c        : {bor_tt_left b}
@@ -93,24 +93,24 @@ theorem band_ff_left (a : bool) : ff && a = ff :=
 refl (ff && a)
 
 theorem band_tt_left (a : bool) : tt && a = a :=
-induction_on a (refl (tt && ff)) (refl (tt && tt))
+cases_on a (refl (tt && ff)) (refl (tt && tt))
 
 theorem band_ff_right (a : bool) : a && ff = ff :=
-induction_on a (refl (ff && ff)) (refl (tt && ff))
+cases_on a (refl (ff && ff)) (refl (tt && ff))
 
 theorem band_tt_right (a : bool) : a && tt = a :=
-induction_on a (refl (ff && tt)) (refl (tt && tt))
+cases_on a (refl (ff && tt)) (refl (tt && tt))
 
 theorem band_id (a : bool) : a && a = a :=
-induction_on a (refl (ff && ff)) (refl (tt && tt))
+cases_on a (refl (ff && ff)) (refl (tt && tt))
 
 theorem band_comm (a b : bool) : a && b = b && a :=
-induction_on a
-  (induction_on b (refl (ff && ff)) (refl (ff && tt)))
-  (induction_on b (refl (tt && ff)) (refl (tt && tt)))
+cases_on a
+  (cases_on b (refl (ff && ff)) (refl (ff && tt)))
+  (cases_on b (refl (tt && ff)) (refl (tt && tt)))
 
 theorem band_assoc (a b c : bool) : (a && b) && c = a && (b && c) :=
-induction_on a
+cases_on a
   (calc (ff && b) && c = ff && c        : {band_ff_left b}
                   ...  = ff             : band_ff_left c
                   ...  = ff && (b && c) : band_ff_left (b && c)⁻¹)
@@ -135,7 +135,7 @@ definition bnot (a : bool) := bool_rec tt ff a
 prefix `!`:85 := bnot
 
 theorem bnot_bnot (a : bool) : !!a = a :=
-induction_on a (refl (!!ff)) (refl (!!tt))
+cases_on a (refl (!!ff)) (refl (!!tt))
 
 theorem bnot_false : !ff = tt := refl _
 
diff --git a/library/standard/data/int/basic.lean b/library/standard/data/int/basic.lean
index d67e8bb7c6..6e09ffd81f 100644
--- a/library/standard/data/int/basic.lean
+++ b/library/standard/data/int/basic.lean
@@ -8,11 +8,6 @@
 import ..nat.basic ..nat.order ..nat.sub ..prod ..quotient ..quotient tools.tactic struc.relation
 import struc.binary
 
--- TODO: show decidability of le and remove this
-import logic.classes.decidable
-import logic.axioms.classical
-import logic.axioms.prop_decidable
-
 import tools.fake_simplifier
 
 namespace int
@@ -214,43 +209,30 @@ exists_intro (pr1 (rep a))
 
 definition of_nat (n : ℕ) : ℤ := psub (pair n 0)
 
+theorem int_eq_decidable [instance] (a b : ℤ) : decidable (a = b) := _
+-- subtype_eq_decidable _ _ (prod_eq_decidable _ _ _ _)
+
 opaque_hint (hiding int)
 coercion of_nat
 
--- TODO: why doesn't the coercion work?
 theorem eq_zero_intro (n : ℕ) : psub (pair n n) = 0 :=
 have H : rel (pair n n) (pair 0 0), by simp,
 eq_abs quotient H
 
--- TODO: this is not a good name -- we want to use abs for the function from int to int.
--- Rename to int.to_nat?
-
--- ## absolute value
-
 definition to_nat : ℤ → ℕ := rec_constant quotient (fun v, dist (pr1 v) (pr2 v))
 
 -- TODO: set binding strength: is this right?
 notation `|`:40 x:40 `|` := to_nat x
 
--- TODO: delete -- prod.destruct should be enough
----move to other library or remove
--- add_rewrite pair_tproj_eq
--- theorem pair_translate {A B : Type} (P : A → B → A × B → Prop)
---   : (∀v, P (pr1 v) (pr2 v) v) ↔ (∀a b, P a b (pair a b)) :=
--- iff_intro
---   (assume H, take a b, subst (by simp) (H (pair a b)))
---   (assume H, take v, subst (by simp) (H (pr1 v) (pr2 v)))
-
-theorem abs_comp (n m : ℕ) : (to_nat (psub (pair n m))) = dist n m :=
+theorem to_nat_comp (n m : ℕ) : (to_nat (psub (pair n m))) = dist n m :=
 have H : ∀v w : ℕ × ℕ, rel v w → dist (pr1 v) (pr2 v) = dist (pr1 w) (pr2 w),
   from take v w H, dist_eq_intro H,
 have H2 : ∀v : ℕ × ℕ, (to_nat (psub v)) = dist (pr1 v) (pr2 v),
   from take v, (comp_constant quotient H (rel_refl v)),
 (by simp) ◂ H2 (pair n m)
 
--- add_rewrite abs_comp --local
+-- add_rewrite to_nat_comp --local
 
---the following theorem includes abs_zero
 theorem to_nat_of_nat (n : ℕ) : to_nat (of_nat n) = n :=
 calc
   (to_nat (psub (pair n 0))) = dist n 0 : by simp
@@ -262,7 +244,7 @@ calc
     ... = to_nat (of_nat m) : {H}
     ... = m : to_nat_of_nat m
 
-theorem abs_eq_zero {a : ℤ} (H : (to_nat a) = 0) : a = 0 :=
+theorem to_nat_eq_zero {a : ℤ} (H : to_nat a = 0) : a = 0 :=
 obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a,
 have H2 : dist xa ya = 0, from
   calc
@@ -275,11 +257,10 @@ calc
 ... = psub (pair ya ya) : {H3}
 ... = 0 : eq_zero_intro ya
 
--- add_rewrite abs_of_nat
+-- add_rewrite to_nat_of_nat
 
 -- ## neg
 
-
 definition neg : ℤ → ℤ := quotient_map quotient flip
 
 -- TODO: is this good?
@@ -309,7 +290,7 @@ theorem neg_inj {a b : ℤ} (H : -a = -b) : a = b :=
 theorem neg_move {a b : ℤ} (H : -a = b) : -b = a :=
 subst H (neg_neg a)
 
-theorem abs_neg (a : ℤ) : (to_nat (-a)) = (to_nat a) :=
+theorem to_nat_neg (a : ℤ) : (to_nat (-a)) = (to_nat a) :=
 obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a,
 by simp
 
@@ -324,7 +305,7 @@ have H5 : n + m = 0, from
       ... = 0 : by simp,
  add_eq_zero H5
 
--- add_rewrite abs_neg
+-- add_rewrite to_nat_neg
 
 ---reverse equalities
 
@@ -354,7 +335,8 @@ or_imp_or (or_swap (proj_zero_or (rep a)))
 opaque_hint (hiding int)
 
 ---rename to by_cases in Lean 0.2 (for now using this to avoid name clash)
-theorem int_by_cases {P : ℤ → Prop} (a : ℤ) (H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-n)) : P a :=
+theorem int_by_cases {P : ℤ → Prop} (a : ℤ) (H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-n)) :
+  P a :=
 or_elim (cases a)
   (assume H, obtain (n : ℕ) (H3 : a = n), from H, subst (symm H3) (H1 n))
   (assume H, obtain (n : ℕ) (H3 : a = -n), from H, subst (symm H3) (H2 n))
@@ -378,7 +360,8 @@ or_elim (cases a)
         have H4 : a = - of_nat (succ k), from subst H3 H2,
         or_intro_right _ (exists_intro k H4)))
 
-theorem int_by_cases_succ {P : ℤ → Prop} (a : ℤ) (H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-of_nat (succ n))) : P a :=
+theorem int_by_cases_succ {P : ℤ → Prop} (a : ℤ)
+  (H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-of_nat (succ n))) : P a :=
 or_elim (cases_succ a)
   (assume H, obtain (n : ℕ) (H3 : a = of_nat n), from H, subst (symm H3) (H1 n))
   (assume H, obtain (n : ℕ) (H3 : a = -of_nat (succ n)), from H, subst (symm H3) (H2 n))
@@ -460,7 +443,8 @@ obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a,
 obtain (xb yb : ℕ) (Hb : b = psub (pair xb yb)), from destruct b,
 by simp
 
-theorem triangle_inequality (a b : ℤ) : (to_nat (a + b)) ≤ (to_nat a) + (to_nat b) := --note: ≤ is nat::≤
+theorem to_nat_add_le (a b : ℤ) : to_nat (a + b) ≤ to_nat a + to_nat b :=
+  --note: ≤ is nat::≤
 obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a,
 obtain (xb yb : ℕ) (Hb : b = psub (pair xb yb)), from destruct b,
 have H : dist (xa + xb) (ya + yb) ≤ dist xa ya + dist xb yb,
@@ -619,24 +603,25 @@ calc
     ... = (to_nat (of_nat n - m)) : sorry -- {symm H}
 
 -- ## mul
--- TODO: remove this when order changes
 theorem rel_mul_prep {xa ya xb yb xn yn xm ym : ℕ}
   (H1 : xa + yb = ya + xb) (H2 : xn + ym = yn + xm)
 : xa * xn + ya * yn + (xb * ym + yb * xm) = xa * yn + ya * xn + (xb * xm + yb * ym) :=
 have H3 : xa * xn + ya * yn + (xb * ym + yb * xm) + (yb * xn + xb * yn + (xb * xn + yb * yn))
-       = xa * yn + ya * xn + (xb * xm + yb * ym) + (yb * xn + xb * yn + (xb * xn + yb * yn)), from
+    = xa * yn + ya * xn + (xb * xm + yb * ym) + (yb * xn + xb * yn + (xb * xn + yb * yn)), from
   calc
     xa * xn + ya * yn + (xb * ym + yb * xm) + (yb * xn + xb * yn + (xb * xn + yb * yn))
-  = xa * xn + yb * xn + (ya * yn + xb * yn) + (xb * xn + xb * ym + (yb * yn + yb * xm)) : by simp
-... = (xa + yb) * xn + (ya + xb) * yn + (xb * (xn + ym) + yb * (yn + xm)) : by simp
-... = (ya + xb) * xn + (xa + yb) * yn + (xb * (yn + xm) + yb * (xn + ym)) : by simp
-... = ya * xn + xb * xn + (xa * yn + yb * yn) + (xb * yn + xb * xm + (yb*xn + yb*ym))
-      : by simp
-... = xa * yn + ya * xn + (xb * xm + yb * ym) + (yb * xn + xb * yn + (xb * xn + yb * yn)) : by simp,
+          = xa * xn + yb * xn + (ya * yn + xb * yn) + (xb * xn + xb * ym + (yb * yn + yb * xm))
+            : by simp
+      ... = (xa + yb) * xn + (ya + xb) * yn + (xb * (xn + ym) + yb * (yn + xm)) : by simp
+      ... = (ya + xb) * xn + (xa + yb) * yn + (xb * (yn + xm) + yb * (xn + ym)) : by simp
+      ... = ya * xn + xb * xn + (xa * yn + yb * yn) + (xb * yn + xb * xm + (yb*xn + yb*ym))
+            : by simp
+      ... = xa * yn + ya * xn + (xb * xm + yb * ym) + (yb * xn + xb * yn + (xb * xn + yb * yn))
+            : by simp,
 nat.add_cancel_right H3
 
-theorem rel_mul {u u' v v' : ℕ × ℕ} (H1 : rel u u') (H2 : rel v v')
-  : rel (pair (pr1 u * pr1 v + pr2 u * pr2 v) (pr1 u * pr2 v + pr2 u * pr1 v))
+theorem rel_mul {u u' v v' : ℕ × ℕ} (H1 : rel u u') (H2 : rel v v') :
+  rel (pair (pr1 u * pr1 v + pr2 u * pr2 v) (pr1 u * pr2 v + pr2 u * pr1 v))
         (pair (pr1 u' * pr1 v' + pr2 u' * pr2 v') (pr1 u' * pr2 v' + pr2 u' * pr1 v')) :=
 calc
     pr1 (pair (pr1 u * pr1 v + pr2 u * pr2 v) (pr1 u * pr2 v + pr2 u * pr1 v))
@@ -651,8 +636,8 @@ definition mul : ℤ → ℤ → ℤ := quotient_map_binary quotient
 
 infixl `*` := int.mul
 
-theorem mul_comp (n m k l : ℕ)
-  : psub (pair n m) * psub (pair k l) = psub (pair (n * k + m * l) (n * l + m * k)) :=
+theorem mul_comp (n m k l : ℕ) :
+  psub (pair n m) * psub (pair k l) = psub (pair (n * k + m * l) (n * l + m * k)) :=
 have H : ∀u v,
     psub u * psub v = psub (pair (pr1 u * pr1 v + pr2 u * pr2 v) (pr1 u * pr2 v + pr2 u * pr1 v)),
   from comp_quotient_map_binary_refl rel_refl quotient @rel_mul,
@@ -671,7 +656,6 @@ obtain (xb yb : ℕ) (Hb : b = psub (pair xb yb)), from destruct b,
 obtain (xc yc : ℕ) (Hc : c = psub (pair xc yc)), from destruct c,
 by simp
 
-
 theorem mul_left_comm : ∀a b c : ℤ, a * (b * c) = b * (a * c) :=
 left_comm mul_comm mul_assoc
 
@@ -709,27 +693,27 @@ subst (mul_comm b a) (subst (mul_comm b (-a)) (mul_neg_right b a))
 theorem mul_neg_neg (a b : ℤ) : -a * -b = a * b :=
 by simp
 
-theorem mul_distr_right (a b c : ℤ) : (a + b) * c = a * c + b * c :=
+theorem mul_right_distr (a b c : ℤ) : (a + b) * c = a * c + b * c :=
 obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a,
 obtain (xb yb : ℕ) (Hb : b = psub (pair xb yb)), from destruct b,
 obtain (xc yc : ℕ) (Hc : c = psub (pair xc yc)), from destruct c,
 by simp
 
-theorem mul_distr_left (a b c : ℤ) : a * (b + c) = a * b + a * c :=
+theorem mul_left_distr (a b c : ℤ) : a * (b + c) = a * b + a * c :=
 calc
   a * (b + c) = (b + c) * a : mul_comm a (b + c)
-    ... = b * a + c * a : mul_distr_right b c a
+    ... = b * a + c * a : mul_right_distr b c a
     ... = a * b + c * a : {mul_comm b a}
     ... = a * b + a * c : {mul_comm c a}
 
-theorem mul_sub_distr_right (a b c : ℤ) : (a - b) * c = a * c - b * c :=
+theorem mul_sub_right_distr (a b c : ℤ) : (a - b) * c = a * c - b * c :=
 calc
-  (a + -b) * c = a * c + -b * c : mul_distr_right a (-b) c
+  (a + -b) * c = a * c + -b * c : mul_right_distr a (-b) c
     ... = a * c + - (b * c) : {mul_neg_left b c}
 
-theorem mul_sub_distr_left (a b c : ℤ) : a * (b - c) = a * b - a * c :=
+theorem mul_sub_left_distr (a b c : ℤ) : a * (b - c) = a * b - a * c :=
 calc
-  a * (b + -c) = a * b + a * -c : mul_distr_left a b (-c)
+  a * (b + -c) = a * b + a * -c : mul_left_distr a b (-c)
     ... = a * b + - (a * c) : {mul_neg_right a c}
 
 theorem mul_of_nat (n m : ℕ) : of_nat n * of_nat m = n * m :=
@@ -745,8 +729,7 @@ by simp
 
 -- add_rewrite mul_zero_left mul_zero_right mul_one_right mul_one_left
 -- add_rewrite mul_comm mul_assoc mul_left_comm
--- add_rewrite mul_distr_right mul_distr_left mul_of_nat
---mul_sub_distr_left mul_sub_distr_right
+-- add_rewrite mul_distr_right mul_distr_left mul_of_nat mul_sub_distr_left mul_sub_distr_right
 
 
 -- ---------- inversion
@@ -759,8 +742,8 @@ have H2 : (to_nat a) * (to_nat b) = 0, from
       ... = 0 : to_nat_of_nat 0,
 have H3 : (to_nat a) = 0 ∨ (to_nat b) = 0, from mul_eq_zero H2,
 or_imp_or H3
-  (assume H : (to_nat a) = 0, abs_eq_zero H)
-  (assume H : (to_nat b) = 0, abs_eq_zero H)
+  (assume H : (to_nat a) = 0, to_nat_eq_zero H)
+  (assume H : (to_nat b) = 0, to_nat_eq_zero H)
 
 theorem mul_cancel_left_or {a b c : ℤ} (H : a * b = a * c) : a = 0 ∨ b = c :=
 have H2 : a * (b - c) = 0, by simp,
@@ -797,29 +780,6 @@ definition le (a b : ℤ) : Prop := ∃n : ℕ, a + n = b
 infix  `<=` := int.le
 infix  `≤`  := int.le
 
--- definition le : ℤ → ℤ → Prop := rec_binary quotient (fun a b, pr1 a + pr2 b ≤ pr2 a + pr1 b)
--- theorem le_comp_alt (u v : ℕ × ℕ) : (psub u ≤ psub v) ↔ (pr1 u + pr2 v ≤ pr2 u + pr1 v)
--- :=
---   comp_binary_refl quotient rel_refl
---   (take u u' v v' : ℕ × ℕ,
---     assume Hu : rel u u',
---     assume Hv : rel v v',)
-
---   u v
-
--- theorem le_intro {a b : ℤ} {n : ℕ} (H : a + of_nat n = b) : a ≤ b
--- :=
---   have lemma : ∀u v, rel (map_pair2 nat::add u (pair n 0)) v → pr1 u + pr2 v + n = pr2 u + pr1 v, from
---     take u v,
---     assume H : rel (map_pair2 nat::add u (pair n 0)) v,
---     calc
---       pr1 u + pr2 v + n = pr1 u + n + pr2 v : nat::add_right_comm (pr1 u) (pr2 v) n
---         ... = pr1 (map_pair2 nat::add u (pair n 0)) + pr2 v : by simp
---         ... = pr2 (map_pair2 nat::add u (pair n 0)) + pr1 v : H
---         ... = pr2 u + 0 + pr1 v : by simp
---         ... = pr2 u + pr1 v : {nat::add_zero_right (pr2 u)},
---   have H2 :
-
 theorem le_intro {a b : ℤ} {n : ℕ} (H : a + n = b) : a ≤ b :=
 exists_intro n H
 
@@ -968,6 +928,12 @@ add_le_cancel_right H
 theorem sub_le_left_inv {a b c : ℤ} (H : c - a ≤ c - b) : b ≤ a :=
 le_neg_inv (add_le_cancel_left H)
 
+theorem le_iff_sub_nonneg (a b : ℤ) : a ≤ b ↔ 0 ≤ b - a :=
+iff_intro
+  (assume H, subst (sub_self _) (sub_le_right H a))
+  (assume H, subst (sub_add_inverse _ _) (subst (add_zero_left _) (add_le_right H a)))
+
+
 -- Less than, Greater than, Greater than or equal
 -- ----------------------------------------------
 
@@ -1208,23 +1174,40 @@ obtain (n : ℕ) (Hn : -a = n), from pos_imp_exists_nat H2,
 have H3 : a = -n, from symm (neg_move Hn),
 exists_intro n H3
 
-theorem abs_pos {a : ℤ} (H : a ≥ 0) : (to_nat a) = a :=
+theorem to_nat_nonneg_eq {a : ℤ} (H : a ≥ 0) : (to_nat a) = a :=
 obtain (n : ℕ) (Hn : a = n), from pos_imp_exists_nat H,
 subst (symm Hn) (congr_arg of_nat (to_nat_of_nat n))
 
---abs_neg is already taken... rename?
-theorem abs_negative {a : ℤ} (H : a ≤ 0) : (to_nat a) = -a :=
+theorem of_nat_nonneg (n : ℕ) : of_nat n ≥ 0 :=
+iff_mp (iff_symm (le_of_nat _ _)) (zero_le _)
+
+theorem le_decidable [instance] {a b : ℤ} : decidable (a ≤ b) :=
+have aux : ∀x, decidable (0 ≤ x), from
+  take x,
+    have H : 0 ≤ x ↔ of_nat (to_nat x) = x, from
+      iff_intro
+        (assume H1, to_nat_nonneg_eq H1)
+        (assume H1, subst H1 (of_nat_nonneg (to_nat x))),
+    decidable_iff_equiv _ (iff_symm H),
+decidable_iff_equiv (aux _) (iff_symm (le_iff_sub_nonneg a b))
+
+theorem ge_decidable [instance] {a b : ℤ} : decidable (a ≥ b)
+theorem lt_decidable [instance] {a b : ℤ} : decidable (a < b)
+theorem gt_decidable [instance] {a b : ℤ} : decidable (a > b)
+
+--to_nat_neg is already taken... rename?
+theorem to_nat_negative {a : ℤ} (H : a ≤ 0) : (to_nat a) = -a :=
 obtain (n : ℕ) (Hn : a = -n), from neg_imp_exists_nat H,
 calc
   (to_nat a) = (to_nat ( -n)) : {Hn}
-  ... = (to_nat n) : {abs_neg n}
+  ... = (to_nat n) : {to_nat_neg n}
   ... = n : {to_nat_of_nat n}
   ... = -a : symm (neg_move (symm Hn))
 
-theorem abs_cases (a : ℤ) : a = (to_nat a) ∨ a = - (to_nat a) :=
+theorem to_nat_cases (a : ℤ) : a = (to_nat a) ∨ a = - (to_nat a) :=
 or_imp_or (le_total 0 a)
-  (assume H : a ≥ 0, symm (abs_pos H))
-  (assume H : a ≤ 0, symm (neg_move (symm (abs_negative H))))
+  (assume H : a ≥ 0, symm (to_nat_nonneg_eq H))
+  (assume H : a ≤ 0, symm (neg_move (symm (to_nat_negative H))))
 
 -- ### interaction of mul with le and lt
 
@@ -1233,7 +1216,7 @@ obtain (n : ℕ) (Hn : b + n = c), from le_elim H,
 have H2 : a * b + of_nat ((to_nat a) * n) = a * c, from
   calc
     a * b + of_nat ((to_nat a) * n) = a * b + (to_nat a) * of_nat n : by simp
-      ... = a * b + a * n : {abs_pos Ha}
+      ... = a * b + a * n : {to_nat_nonneg_eq Ha}
       ... = a * (b + n) : by simp
       ... = a * c : by simp,
 le_intro H2
@@ -1339,7 +1322,7 @@ have H2 : (to_nat a) * (to_nat b) = 1, from
       ... = (to_nat 1) : {H}
       ... = 1 : to_nat_of_nat 1,
 have H3 : (to_nat a) = 1, from mul_eq_one_left H2,
-or_imp_or (abs_cases a)
+or_imp_or (to_nat_cases a)
   (assume H4 : a = (to_nat a), subst H3 H4)
   (assume H4 : a = - (to_nat a), subst H3 H4)
 
@@ -1365,7 +1348,7 @@ trans (if_neg (lt_antisym H) _ _) (if_pos H  _ _)
 theorem sign_zero : sign 0 = 0 :=
 trans (if_neg (lt_irrefl 0) _ _) (if_neg (lt_irrefl 0)  _ _)
 
--- add_rewrite sign_negative sign_pos abs_negative abs_pos sign_zero mul_abs
+-- add_rewrite sign_negative sign_pos to_nat_negative to_nat_nonneg_eq sign_zero mul_to_nat
 
 theorem mul_sign_to_nat (a : ℤ) : sign a * (to_nat a) = a :=
 have temp1 : ∀a : ℤ, a < 0 → a ≤ 0, from take a, lt_imp_le,
@@ -1390,7 +1373,7 @@ or_elim (em (a = 0))
               ... = sign a * (to_nat a) * (sign b * (to_nat b)) : {symm (mul_sign_to_nat b)}
               ... = sign a * sign b  * (to_nat (a * b)) : by simp,
         have H2 : (to_nat (a * b)) ≠ 0, from
-          take H2', mul_ne_zero Ha Hb (abs_eq_zero H2'),
+          take H2', mul_ne_zero Ha Hb (to_nat_eq_zero H2'),
         have H3 : (to_nat (a * b)) ≠ of_nat 0, from contrapos of_nat_inj H2,
         mul_cancel_right H3 H))
 
@@ -1418,7 +1401,7 @@ or_elim3 (trichotomy a 0) sorry sorry sorry
 
 -- add_rewrite sign_neg
 
-theorem abs_sign_ne_zero {a : ℤ} (H : a ≠ 0) : (to_nat (sign a)) = 1 :=
+theorem to_nat_sign_ne_zero {a : ℤ} (H : a ≠ 0) : (to_nat (sign a)) = 1 :=
 or_elim3 (trichotomy a 0) sorry
 --  (by simp)
   (assume H2 : a = 0, absurd_elim _ H2 H)
diff --git a/library/standard/data/int/default.lean b/library/standard/data/int/default.lean
index 09e23846e3..8671898983 100644
--- a/library/standard/data/int/default.lean
+++ b/library/standard/data/int/default.lean
@@ -2,4 +2,4 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Jeremy Avigad
 
-import data.nat.basic
+import data.int.basic
diff --git a/library/standard/data/nat/div.lean b/library/standard/data/nat/div.lean
index 56df2e6495..1e42ab7fa0 100644
--- a/library/standard/data/nat/div.lean
+++ b/library/standard/data/nat/div.lean
@@ -24,16 +24,6 @@ using fake_simplifier decidable
 
 namespace nat
 
-
--- TODO: settle on a name, and move this
-theorem by_cases (a : Prop) {b : Prop} {C : decidable a} (Hab : a → b) (Hnab : ¬a → b) : b :=
-or_elim (em a) (assume Ha, Hab Ha) (assume Hna, Hnab Hna)
-
--- move to nat
-theorem pos_imp_ne_zero {n : ℕ} (H : n > 0) : n ≠ 0 :=
-ne_symm (lt_imp_ne H)
-
-
 -- A general recursion principle
 -- =============================
 --
@@ -102,7 +92,7 @@ case_strong_induction_on m
     funext
       (take x : dom,
         show f' (succ m) x = restrict default measure f (succ m) x, from
-          by_cases (measure x < succ m)
+          by_cases -- (measure x < succ m)
             (assume H1 : measure x < succ m,
               have H2 [fact] : f' (succ m) x = rec_val x f, from
                 calc
@@ -165,14 +155,14 @@ theorem div_aux_decreasing (y : ℕ) (g : ℕ → ℕ) (m : ℕ) (x : ℕ) (H :
 let lhs := div_aux_rec y x g in
 let rhs := div_aux_rec y x (restrict 0 (fun x, x) g m) in
 show lhs = rhs, from
-  by_cases (y = 0 ∨ x < y)
+  by_cases -- (y = 0 ∨ x < y)
     (assume H1 : y = 0 ∨ x < y,
       calc
         lhs = 0 : if_pos H1 _ _
           ... = rhs : symm (if_pos H1 _ _))
     (assume H1 : ¬ (y = 0 ∨ x < y),
       have H2 : y ≠ 0 ∧ ¬ x < y, from not_or _ _ ◂ H1,
-      have ypos : y > 0, from ne_zero_pos (and_elim_left H2),
+      have ypos : y > 0, from ne_zero_imp_pos (and_elim_left H2),
       have xgey : x ≥ y, from not_lt_imp_ge (and_elim_right H2),
       have H4 : x - y < x, from sub_lt (lt_le_trans ypos xgey) ypos,
       have H5 : x - y < m, from lt_le_trans H4 H,
@@ -241,14 +231,14 @@ theorem mod_aux_decreasing (y : ℕ) (g : ℕ → ℕ) (m : ℕ) (x : ℕ) (H :
 let lhs := mod_aux_rec y x g in
 let rhs := mod_aux_rec y x (restrict 0 (fun x, x) g m) in
 show lhs = rhs, from
-  by_cases (y = 0 ∨ x < y)
+  by_cases -- (y = 0 ∨ x < y)
     (assume H1 : y = 0 ∨ x < y,
       calc
         lhs = x : if_pos H1 _ _
           ... = rhs : symm (if_pos H1 _ _))
     (assume H1 : ¬ (y = 0 ∨ x < y),
       have H2 : y ≠ 0 ∧ ¬ x < y, from not_or _ _ ◂ H1,
-      have ypos : y > 0, from ne_zero_pos (and_elim_left H2),
+      have ypos : y > 0, from ne_zero_imp_pos (and_elim_left H2),
       have xgey : x ≥ y, from not_lt_imp_ge (and_elim_right H2),
       have H4 : x - y < x, from sub_lt (lt_le_trans ypos xgey) ypos,
       have H5 : x - y < m, from lt_le_trans H4 H,
@@ -325,7 +315,7 @@ case_strong_induction_on x
   (take x,
     assume IH : ∀x', x' ≤ x → x' mod y < y,
     show succ x mod y < y, from
-      by_cases (succ x < y)
+      by_cases -- (succ x < y)
         (assume H1 : succ x < y,
           have H2 : succ x mod y = succ x, from mod_lt_eq H1,
           show succ x mod y < y, from subst (symm H2) H1)
@@ -351,7 +341,7 @@ case_zero_pos y
         (take x,
           assume IH : ∀x', x' ≤ x → x' = x' div y * y + x' mod y,
           show succ x = succ x div y * y + succ x mod y, from
-            by_cases (succ x < y)
+            by_cases -- (succ x < y)
               (assume H1 : succ x < y,
                 have H2 : succ x div y = 0, from div_less H1,
                 have H3 : succ x mod y = succ x, from mod_lt_eq H1,
@@ -393,10 +383,10 @@ have H6 : y > 0, from le_lt_trans (zero_le _) H1,
 show q1 = q2, from mul_cancel_right H6 H5
 
 theorem div_mul_mul {z : ℕ} (x y : ℕ) (zpos : z > 0) : (z * x) div (z * y) = x div y :=
-by_cases (y = 0)
+by_cases -- (y = 0)
   (assume H : y = 0, by simp)
   (assume H : y ≠ 0,
-    have ypos : y > 0, from ne_zero_pos H,
+    have ypos : y > 0, from ne_zero_imp_pos H,
     have zypos : z * y > 0, from mul_pos zpos ypos,
     have H1 : (z * x) mod (z * y) < z * y, from mod_lt _ zypos,
     have H2 : z * (x mod y) < z * y, from mul_lt_left zpos (mod_lt _ ypos),
@@ -410,10 +400,10 @@ by_cases (y = 0)
 ---            ... = (x div y) * (z * y) + z * (x mod y) : by simp))
 
 theorem mod_mul_mul {z : ℕ} (x y : ℕ) (zpos : z > 0) : (z * x) mod (z * y) = z * (x mod y) :=
-by_cases (y = 0)
+by_cases -- (y = 0)
   (assume H : y = 0, by simp)
   (assume H : y ≠ 0,
-    have ypos : y > 0, from ne_zero_pos H,
+    have ypos : y > 0, from ne_zero_imp_pos H,
     have zypos : z * y > 0, from mul_pos zpos ypos,
     have H1 : (z * x) mod (z * y) < z * y, from mod_lt _ zypos,
     have H2 : z * (x mod y) < z * y, from mul_lt_left zpos (mod_lt _ ypos),
@@ -477,7 +467,7 @@ have H2 : (z - x div y) * y = x mod y, from
        ... = x mod y + x div y * y - x div y * y : {H1}
        ... = x mod y : sub_add_left _ _,
 show x mod y = 0, from
-  by_cases (y = 0)
+  by_cases -- (y = 0)
     (assume yz : y = 0,
       have xz : x = 0, from
         calc
@@ -489,7 +479,7 @@ show x mod y = 0, from
           ... = x : mod_zero _
           ... = 0 : xz)
     (assume ynz : y ≠ 0,
-      have ypos : y > 0, from ne_zero_pos ynz,
+      have ypos : y > 0, from ne_zero_imp_pos ynz,
       have H3 : (z - x div y) * y < y, from subst (symm H2) (mod_lt x ypos),
       have H4 : (z - x div y) * y < 1 * y, from subst (symm (mul_one_left y)) H3,
       have H5 : z - x div y < 1, from mul_lt_cancel_right H4,
@@ -578,7 +568,7 @@ theorem dvd_add_cancel_right {m n1 n2 : ℕ} (H : m | (n1 + n2)) : m | n2 → m
 dvd_add_cancel_left (subst (add_comm _ _) H)
 
 theorem dvd_sub {m n1 n2 : ℕ} (H1 : m | n1) (H2 : m | n2) : m | (n1 - n2) :=
-by_cases _
+by_cases
   (assume H3 : n1 ≥ n2,
     have H4 : n1 = n1 - n2 + n2, from symm (add_sub_ge_left H3),
     show m | n1 - n2, from dvd_add_cancel_right (subst H4 H1) H2)
@@ -608,13 +598,13 @@ let p' := pair y (x mod y) in
 let lhs := gcd_aux_rec p g in
 let rhs := gcd_aux_rec p (restrict 0 gcd_aux_measure g m) in
 show lhs = rhs, from
-  by_cases (y = 0)
+  by_cases -- (y = 0)
     (assume H1 : y = 0,
       calc
         lhs = x : if_pos H1 _ _
           ... = rhs : symm (if_pos H1 _ _))
     (assume H1 : y ≠ 0,
-      have ypos : y > 0, from ne_zero_pos H1,
+      have ypos : y > 0, from ne_zero_imp_pos H1,
       have H2 : gcd_aux_measure p' = x mod y, from pr2_pair _ _,
       have H3 : gcd_aux_measure p' < gcd_aux_measure p, from subst (symm H2) (mod_lt _ ypos),
       have H4: gcd_aux_measure p' < m, from lt_le_trans H3 H,
diff --git a/library/standard/data/nat/order.lean b/library/standard/data/nat/order.lean
index 69589b4ec5..51e1fce207 100644
--- a/library/standard/data/nat/order.lean
+++ b/library/standard/data/nat/order.lean
@@ -276,12 +276,6 @@ infix `>` : 50 := gt
 
 theorem lt_def (n m : ℕ) : (n < m) = (succ n ≤ m) := refl (n < m)
 
--- theorem gt_def (n m : ℕ) : n > m ↔ m < n
--- := refl (n > m)
-
--- theorem ge_def (n m : ℕ) : n ≥ m ↔ m ≤ n
--- := refl (n ≥ m)
-
 -- add_rewrite gt_def ge_def --it might be possible to remove this in Lean 0.2
 
 theorem lt_intro {n m k : ℕ} (H : succ n + k = m) : n < m :=
@@ -491,9 +485,12 @@ or_imp_or_left (or_swap (le_imp_lt_or_eq (zero_le n))) (take H : 0 = n, symm H)
 theorem succ_imp_pos {n m : ℕ} (H : n = succ m) : n > 0 :=
 H⁻¹ ▸ (succ_pos m)
 
-theorem ne_zero_pos {n : ℕ} (H : n ≠ 0) : n > 0 :=
+theorem ne_zero_imp_pos {n : ℕ} (H : n ≠ 0) : n > 0 :=
 or_elim (zero_or_pos n) (take H2 : n = 0, absurd_elim _ H2 H) (take H2 : n > 0, H2)
 
+theorem pos_imp_ne_zero {n : ℕ} (H : n > 0) : n ≠ 0 :=
+ne_symm (lt_imp_ne H)
+
 theorem pos_imp_eq_succ {n : ℕ} (H : n > 0) : exists l, n = succ l :=
 lt_imp_eq_succ H
 
@@ -606,4 +603,5 @@ mul_eq_one_left ((mul_comm n m) ▸ H)
 
 --- theorem mul_eq_one {n m : ℕ} (H : n * m = 1) : n = 1 ∧ m = 1
 --- := and_intro (mul_eq_one_left H) (mul_eq_one_right H)
+
 end nat
diff --git a/library/standard/data/prod.lean b/library/standard/data/prod.lean
index 6be995d825..9a0e1a319c 100644
--- a/library/standard/data/prod.lean
+++ b/library/standard/data/prod.lean
@@ -2,9 +2,9 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad
 
-import logic.classes.inhabited logic.connectives.eq
+import logic.classes.inhabited logic.connectives.eq logic.classes.decidable
 
-using inhabited
+using inhabited decidable
 
 inductive prod (A B : Type) : Type :=
 | pair : A → B → prod A B
@@ -43,8 +43,17 @@ section
   theorem prod_inhabited (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) :=
   inhabited_destruct H1 (λa, inhabited_destruct H2 (λb, inhabited_mk (pair a b)))
 
+  theorem prod_eq_decidable (u v : A × B) (H1 : decidable (pr1 u = pr1 v))
+      (H2 : decidable (pr2 u = pr2 v)) : decidable (u = v) :=
+    have H3 : u = v ↔ (pr1 u = pr1 v) ∧ (pr2 u = pr2 v), from
+      iff_intro
+	(assume H, subst H (and_intro (refl _) (refl _)))
+	(assume H, and_elim H (assume H4 H5, prod_eq H4 H5)),
+    decidable_iff_equiv _ (iff_symm H3)
+
 end
 
 instance prod_inhabited
+instance prod_eq_decidable
 
 end prod
diff --git a/library/standard/data/quotient/basic.lean b/library/standard/data/quotient/basic.lean
index 4d1bf31f57..16cbcd1d72 100644
--- a/library/standard/data/quotient/basic.lean
+++ b/library/standard/data/quotient/basic.lean
@@ -126,8 +126,8 @@ have H2 [fact] : R a (rep (abs a)), from R_rep_abs Q Ha,
 calc
   rec Q f (abs a) =  eq_rec_on _ (f (rep (abs a))) : rfl
     ... = eq_rec_on _ (eq_rec_on _ (f a)) : {symm (H _ _ H2)}
-    ... = eq_rec_on _ (f a) : eq_rec_on_compose _ _ _
-    ... = f a : eq_rec_on_id _ _
+    ... = eq_rec_on _ (f a) : eq_rec_on_compose (eq_abs Q H2) _ _
+    ... = f a : eq_rec_on_id (trans (eq_abs Q H2) (abs_rep Q (abs a))) _
 
 definition rec_constant {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
   (Q : is_quotient R abs rep) {C : Type} (f : A → C) (b : B) : C :=
diff --git a/library/standard/data/sigma.lean b/library/standard/data/sigma.lean
index 6ef6584a22..744fa7e3f4 100644
--- a/library/standard/data/sigma.lean
+++ b/library/standard/data/sigma.lean
@@ -48,7 +48,7 @@ section
     ∀(H1 : dpr1 p1 = dpr1 p2) (H2 : eq_rec_on H1 (dpr2 p1) = (dpr2 p2)), p1 = p2 :=
   sigma_destruct p1 (take a1 b1, sigma_destruct p2 (take a2 b2 H1 H2, dpair_eq H1 H2))
 
-  theorem sigma_inhabited (H1 : inhabited A) (H2 : inhabited (B (default A))) :
+  theorem sigma_inhabited [instance] (H1 : inhabited A) (H2 : inhabited (B (default A))) :
     inhabited (sigma B) :=
    inhabited_destruct H1 (λa, inhabited_destruct H2 (λb, inhabited_mk (dpair (default A) b)))
 
diff --git a/library/standard/data/subtype.lean b/library/standard/data/subtype.lean
index 1743aa87a6..c2ab191106 100644
--- a/library/standard/data/subtype.lean
+++ b/library/standard/data/subtype.lean
@@ -2,7 +2,9 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad
 
-import logic.classes.inhabited logic.connectives.eq
+import logic.classes.inhabited logic.connectives.eq logic.classes.decidable
+
+using decidable
 
 inductive subtype {A : Type} (P : A → Prop) : Type :=
 | tag : Πx : A, P x → subtype P
@@ -36,10 +38,18 @@ section
   theorem subtype_eq {a1 a2 : {x | P x}} : ∀(H : elt_of a1 = elt_of a2), a1 = a2 :=
   subtype_destruct a1 (take x1 H1, subtype_destruct a2 (take x2 H2 H, tag_eq H))
 
-  -- TODO: need inhabited
+  theorem subtype_inhabited {a : A} (H : P a) : inhabited {x | P x} :=
+  inhabited_mk (tag a H)
+
+  theorem subtype_eq_decidable (a1 a2 : {x | P x})
+    (H : decidable (elt_of a1 = elt_of a2)) : decidable (a1 = a2) :=
+  have H1 : (a1 = a2) ↔ (elt_of a1 = elt_of a2), from
+    iff_intro (assume H, subst H rfl) (assume H, subtype_eq H),
+  decidable_iff_equiv _ (iff_symm H1)
 
 end
 
-end subtype
+instance subtype_inhabited
+instance subtype_eq_decidable
 
--- instance subtype_inhabited
+end subtype
diff --git a/library/standard/data/sum.lean b/library/standard/data/sum.lean
index 2314072f78..92c059ca4d 100644
--- a/library/standard/data/sum.lean
+++ b/library/standard/data/sum.lean
@@ -1,18 +1,33 @@
-----------------------------------------------------------------------------------------------------
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Leonardo de Moura
-----------------------------------------------------------------------------------------------------
+-- Author: Leonardo de Moura, Jeremy Avigad
 
-import logic.connectives.prop
+import logic.connectives.prop logic.classes.inhabited logic.classes.decidable
+
+using inhabited decidable
 
 namespace sum
+
+-- TODO: take this outside the namespace when the inductive package handles it better
 inductive sum (A B : Type) : Type :=
 | inl : A → sum A B
 | inr : B → sum A B
 
 infixr `+`:25 := sum
 
-theorem induction_on {A B : Type} {C : Prop} (s : A + B) (H1 : A → C) (H2 : B → C) : C :=
+theorem cases_on {A B : Type} {C : Prop} (s : A + B) (H1 : A → C) (H2 : B → C) : C :=
 sum_rec H1 H2 s
+
+-- TODO: need equality lemmas
+-- theorem inl_eq {A : Type} (B : Type) {a1 a2 : A} (H : inl B a1 = inl B a2) : a1 = a2 := sorry
+
+theorem sum_inhabited_left [instance] {A B : Type} (H : inhabited A) : inhabited (A + B) :=
+inhabited_mk (inl B (default A))
+
+theorem sum_inhabited_right [instance] {A B : Type} (H : inhabited B) : inhabited (A + B) :=
+inhabited_mk (inr A (default B))
+
+--theorem sum_eq_decidable [instance] {A B : Type} (s1 s2 : A + B) : decidable (s1 = s2) :=
+--cases_
+
 end sum
\ No newline at end of file
diff --git a/library/standard/logic/classes/decidable.lean b/library/standard/logic/classes/decidable.lean
index f77b6eabea..3a27001597 100644
--- a/library/standard/logic/classes/decidable.lean
+++ b/library/standard/logic/classes/decidable.lean
@@ -1,8 +1,6 @@
-----------------------------------------------------------------------------------------------------
 -- 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 logic.connectives.basic logic.connectives.eq
 
@@ -12,16 +10,17 @@ inductive decidable (p : Prop) : Type :=
 | inl : p  → decidable p
 | inr : ¬p → decidable p
 
-theorem decidable_true [instance] : decidable true :=
+theorem true_decidable [instance] : decidable true :=
 inl trivial
 
-theorem decidable_false [instance] : decidable false :=
+theorem false_decidable [instance] : decidable false :=
 inr not_false_trivial
 
 theorem induction_on {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C :=
 decidable_rec H1 H2 H
 
-definition rec_on [inline] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C :=
+definition rec_on [inline] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) :
+  C :=
 decidable_rec H1 H2 H
 
 theorem irrelevant {p : Prop} (d1 d2 : decidable p) : d1 = d2 :=
@@ -39,40 +38,48 @@ decidable_rec
 theorem em (p : Prop) {H : decidable p} : p ∨ ¬p :=
 induction_on H (λ Hp, or_inl Hp) (λ Hnp, or_inr Hnp)
 
+theorem by_cases {a b : Prop} {C : decidable a} (Hab : a → b) (Hnab : ¬a → b) : b :=
+or_elim (em a) (assume Ha, Hab Ha) (assume Hna, Hnab Hna)
+
 theorem by_contradiction {p : Prop} {Hp : decidable p} (H : ¬p → false) : p :=
 or_elim (em p)
   (assume H1 : p, H1)
   (assume H1 : ¬p, false_elim p (H H1))
 
-theorem decidable_and [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∧ b) :=
+theorem and_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
+  decidable (a ∧ b) :=
 rec_on Ha
   (assume Ha  : a, rec_on Hb
     (assume Hb  : b,  inl (and_intro Ha Hb))
     (assume Hnb : ¬b, inr (and_not_right a Hnb)))
   (assume Hna : ¬a, inr (and_not_left b Hna))
 
-theorem decidable_or [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∨ b) :=
+theorem or_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
+  decidable (a ∨ b) :=
 rec_on Ha
   (assume Ha  : a, inl (or_inl Ha))
   (assume Hna : ¬a, rec_on Hb
     (assume Hb  : b,  inl (or_inr Hb))
     (assume Hnb : ¬b, inr (or_not_intro Hna Hnb)))
 
-theorem decidable_not [instance] {a : Prop} (Ha : decidable a) : decidable (¬a) :=
+theorem not_decidable [instance] {a : Prop} (Ha : decidable a) : decidable (¬a) :=
 rec_on Ha
   (assume Ha,  inr (not_not_intro Ha))
   (assume Hna, inl Hna)
 
-theorem decidable_iff [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ↔ b) :=
+theorem iff_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
+  decidable (a ↔ b) :=
 rec_on Ha
   (assume Ha, rec_on Hb
     (assume Hb  : b,  inl (iff_intro (assume H, Hb) (assume H, Ha)))
     (assume Hnb : ¬b, inr (assume H : a ↔ b, absurd (iff_elim_left H Ha) Hnb)))
   (assume Hna, rec_on Hb
     (assume Hb  : b,  inr (assume H : a ↔ b, absurd (iff_elim_right H Hb) Hna))
-    (assume Hnb : ¬b, inl (iff_intro (assume Ha, absurd_elim b Ha Hna) (assume Hb, absurd_elim a Hb Hnb))))
+    (assume Hnb : ¬b, inl
+	(iff_intro (assume Ha, absurd_elim b Ha Hna) (assume Hb, absurd_elim a Hb Hnb))))
 
-theorem decidable_implies [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a → b) :=
+theorem implies_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
+  decidable (a → b) :=
 rec_on Ha
   (assume Ha  : a, rec_on Hb
     (assume Hb  : b,  inl (assume H, Hb))