diff --git a/library/standard/data/bool/basic.lean b/library/standard/data/bool.lean
similarity index 95%
rename from library/standard/data/bool/basic.lean
rename to library/standard/data/bool.lean
index c65c771a0..c1b2edc86 100644
--- a/library/standard/data/bool/basic.lean
+++ b/library/standard/data/bool.lean
@@ -2,8 +2,12 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 
-import .type logic.connectives.basic logic.classes.decidable logic.classes.inhabited
-using eq_proofs decidable
+import logic.connectives.basic logic.classes.decidable logic.classes.inhabited
+using eq_ops decidable
+
+inductive bool : Type :=
+| ff : bool
+| tt : bool
 
 namespace bool
 
@@ -11,7 +15,7 @@ theorem induction_on {p : bool → Prop} (b : bool) (H0 : p ff) (H1 : p tt) : p
 bool_rec H0 H1 b
 
 theorem inhabited_bool [instance] : inhabited bool :=
-inhabited_intro ff
+inhabited_mk ff
 
 definition cond {A : Type} (b : bool) (t e : A) :=
 bool_rec e t b
@@ -136,4 +140,4 @@ theorem bnot_false : !ff = tt := refl _
 
 theorem bnot_true  : !tt = ff := refl _
 
-end bool
\ No newline at end of file
+end bool
diff --git a/library/standard/data/bool/bool.md b/library/standard/data/bool/bool.md
deleted file mode 100644
index fc04a9eee..000000000
--- a/library/standard/data/bool/bool.md
+++ /dev/null
@@ -1,7 +0,0 @@
-data.bool
-=========
-
-The type of booleans.
-
-* [type](type.lean) : the datatype
-* [basic](basic.lean) : basic properties
diff --git a/library/standard/data/bool/type.lean b/library/standard/data/bool/type.lean
deleted file mode 100644
index c4a387706..000000000
--- a/library/standard/data/bool/type.lean
+++ /dev/null
@@ -1,11 +0,0 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Leonardo de Moura
-
-namespace bool
-
-inductive bool : Type :=
-| ff : bool
-| tt : bool
-
-end bool
\ No newline at end of file
diff --git a/library/standard/data/data.md b/library/standard/data/data.md
index 1b713efa0..78d1b8979 100644
--- a/library/standard/data/data.md
+++ b/library/standard/data/data.md
@@ -7,7 +7,7 @@ Basic types:
 
 * [empty](empty.lean) : the empty type
 * [unit](unit.lean) : the singleton type
-* [bool](bool/bool.md) : the boolean values
+* [bool](bool.lean) : the boolean values
 * [num](num.lean) : generic numerals
 * [string](string.lean) : ascii strings
 * [nat](nat/nat.md) : the natural numbers
@@ -20,5 +20,6 @@ Constructors:
 * [sigma](sigma.lean) : the dependent product
 * [option](option.lean)
 * [subtype](subtype.lean)
+* [quotient](quotient/quotient.md)
 * [list](list/list.md)
 * [set](set.lean)
\ No newline at end of file
diff --git a/library/standard/data/default.lean b/library/standard/data/default.lean
new file mode 100644
index 000000000..634a88493
--- /dev/null
+++ b/library/standard/data/default.lean
@@ -0,0 +1,6 @@
+--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+--- Released under Apache 2.0 license as described in the file LICENSE.
+--- Author: Jeremy Avigad
+
+import .empty .unit .bool .num .string .nat .int
+import .prod .sum .sigma .option .subtype .quotient .list .set
diff --git a/library/standard/data/int/basic.lean b/library/standard/data/int/basic.lean
new file mode 100644
index 000000000..d0773d9cb
--- /dev/null
+++ b/library/standard/data/int/basic.lean
@@ -0,0 +1,1460 @@
+-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Floris van Doorn
+
+-- Theory int
+-- ==========
+
+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
+using nat (hiding case)
+using quotient
+using subtype
+using prod
+using relation
+using decidable
+using binary
+
+using fake_simplifier
+
+
+-- ## The defining equivalence relation on ℕ × ℕ
+
+abbreviation rel (a b : ℕ × ℕ) : Prop :=  pr1 a + pr2 b = pr2 a + pr1 b
+
+theorem rel_comp (n m k l : ℕ) : (rel (pair n m) (pair k l)) ↔ (n + l = m + k) :=
+have H : (pr1 (pair n m) + pr2 (pair k l) = pr2 (pair n m) + pr1 (pair k l)) ↔ (n + l = m + k),
+  by simp, 
+H
+
+-- add_rewrite rel_comp --local
+
+theorem rel_refl (a : ℕ × ℕ) : rel a a :=
+add_comm (pr1 a) (pr2 a)
+
+theorem rel_symm {a b : ℕ × ℕ} (H : rel a b) : rel b a :=
+calc
+  pr1 b + pr2 a = pr2 a + pr1 b : add_comm _ _
+    ... = pr1 a + pr2 b : symm H
+    ... = pr2 b + pr1 a : add_comm _ _
+
+theorem rel_trans {a b c : ℕ × ℕ} (H1 : rel a b) (H2 : rel b c) : rel a c :=
+have H3 : pr1 a + pr2 c + pr2 b = pr2 a + pr1 c + pr2 b, from
+  calc
+   pr1 a + pr2 c + pr2 b = pr1 a + pr2 b + pr2 c : by simp
+    ... = pr2 a + pr1 b + pr2 c : {H1}
+    ... = pr2 a + (pr1 b + pr2 c) : by simp
+    ... = pr2 a + (pr2 b + pr1 c) : {H2}
+    ... = pr2 a + pr1 c + pr2 b : by simp,
+show pr1 a + pr2 c = pr2 a + pr1 c, from add_cancel_right H3
+
+theorem rel_equiv : is_equivalence rel :=
+is_equivalence_mk (is_reflexive_mk rel_refl) (is_symmetric_mk @rel_symm) 
+(is_transitive_mk @rel_trans)
+
+theorem rel_flip {a b : ℕ × ℕ} (H : rel a b) : rel (flip a) (flip b) :=
+calc
+  pr1 (flip a) + pr2 (flip b) = pr2 a + pr1 b : by simp
+    ... = pr1 a + pr2 b : symm H
+    ... = pr2 (flip a) + pr1 (flip b) : by simp
+
+-- ## The canonical representative of each equivalence class
+
+definition proj (a : ℕ × ℕ) : ℕ × ℕ :=
+if pr1 a ≥ pr2 a then pair (pr1 a - pr2 a) 0 else pair 0 (pr2 a - pr1 a)
+
+theorem proj_ge {a : ℕ × ℕ} (H : pr1 a ≥ pr2 a) : proj a = pair (pr1 a - pr2 a) 0 :=
+if_pos H _ _
+
+theorem proj_lt {a : ℕ × ℕ} (H : pr1 a < pr2 a) : proj a = pair 0 (pr2 a - pr1 a) :=
+have H2 : ¬ pr1 a ≥ pr2 a, from lt_imp_not_ge H,
+if_neg H2 _ _
+
+theorem proj_le {a : ℕ × ℕ} (H : pr1 a ≤ pr2 a) : proj a = pair 0 (pr2 a - pr1 a) :=
+or_elim (le_or_gt (pr2 a) (pr1 a))
+  (assume H2 : pr2 a ≤ pr1 a,
+    have H3 : pr1 a = pr2 a, from le_antisym H H2,
+    calc
+      proj a = pair (pr1 a - pr2 a) 0 : proj_ge H2
+	... = pair (pr1 a - pr2 a) (pr1 a - pr1 a) : {symm (sub_self (pr1 a))}
+	... = pair (pr2 a - pr2 a) (pr2 a - pr1 a) : {H3}
+	... = pair 0 (pr2 a - pr1 a) : {sub_self (pr2 a)})
+  (assume H2 : pr1 a < pr2 a, proj_lt H2)
+
+theorem proj_ge_pr1 {a : ℕ × ℕ} (H : pr1 a ≥ pr2 a) : pr1 (proj a) = pr1 a - pr2 a :=
+calc
+  pr1 (proj a) = pr1 (pair (pr1 a - pr2 a) 0) : {proj_ge H}
+    ... = pr1 a - pr2 a : pr1_pair (pr1 a - pr2 a) 0
+
+theorem proj_ge_pr2 {a : ℕ × ℕ} (H : pr1 a ≥ pr2 a) : pr2 (proj a) = 0 :=
+calc
+  pr2 (proj a) = pr2 (pair (pr1 a - pr2 a) 0) : {proj_ge H}
+    ... = 0 : pr2_pair (pr1 a - pr2 a) 0
+
+theorem proj_le_pr1 {a : ℕ × ℕ} (H : pr1 a ≤ pr2 a) : pr1 (proj a) = 0 :=
+calc
+  pr1 (proj a) = pr1 (pair 0 (pr2 a - pr1 a)) : {proj_le H}
+    ... = 0 : pr1_pair 0 (pr2 a - pr1 a)
+
+theorem proj_le_pr2 {a : ℕ × ℕ} (H : pr1 a ≤ pr2 a) : pr2 (proj a) = pr2 a - pr1 a :=
+calc
+  pr2 (proj a) = pr2 (pair 0 (pr2 a - pr1 a)) : {proj_le H}
+    ... = pr2 a - pr1 a : pr2_pair 0 (pr2 a - pr1 a)
+
+theorem proj_flip (a : ℕ × ℕ) : proj (flip a) = flip (proj a) :=
+have special : ∀a, pr2 a ≤ pr1 a → proj (flip a) = flip (proj a), from
+  take a,
+  assume H : pr2 a ≤ pr1 a,
+  have H2 : pr1 (flip a) ≤ pr2 (flip a), from P_flip H,
+  have H3 : pr1 (proj (flip a)) = pr1 (flip (proj a)), from
+    calc
+      pr1 (proj (flip a)) = 0 : proj_le_pr1 H2
+	... = pr2 (proj a) : symm (proj_ge_pr2 H)
+	... = pr1 (flip (proj a)) : symm (flip_pr1 (proj a)),
+  have H4 : pr2 (proj (flip a)) = pr2 (flip (proj a)), from
+    calc
+      pr2 (proj (flip a)) = pr2 (flip a) - pr1 (flip a) : proj_le_pr2 H2
+	... = pr1 a - pr1 (flip a) : {flip_pr2 a}
+	... = pr1 a - pr2 a : {flip_pr1 a}
+	... = pr1 (proj a) : symm (proj_ge_pr1 H)
+	... = pr2 (flip (proj a)) : symm (flip_pr2 (proj a)),
+  prod_eq H3 H4,
+or_elim (le_total (pr2 a) (pr1 a))
+  (assume H : pr2 a ≤ pr1 a, special a H)
+  (assume H : pr1 a ≤ pr2 a,
+    have H2 : pr2 (flip a) ≤ pr1 (flip a), from P_flip H,
+    calc
+      proj (flip a) = flip (flip (proj (flip a))) : symm (flip_flip (proj (flip a)))
+	... = flip (proj (flip (flip a))) : {symm (special (flip a) H2)}
+	... = flip (proj a) : {flip_flip a})
+
+theorem proj_rel (a : ℕ × ℕ) : rel a (proj a) :=
+or_elim (le_total (pr2 a) (pr1 a))
+  (assume H : pr2 a ≤ pr1 a,
+    calc
+      pr1 a + pr2 (proj a) = pr1 a + 0 : {proj_ge_pr2 H}
+	... = pr1 a : add_zero_right (pr1 a)
+	... = pr2 a + (pr1 a - pr2 a) : symm (add_sub_le H)
+	... = pr2 a + pr1 (proj a) : {symm (proj_ge_pr1 H)})
+  (assume H : pr1 a ≤ pr2 a,
+    calc
+      pr1 a + pr2 (proj a) = pr1 a + (pr2 a - pr1 a) : {proj_le_pr2 H}
+	... = pr2 a : add_sub_le H
+	... = pr2 a + 0 : symm (add_zero_right (pr2 a))
+	... = pr2 a + pr1 (proj a) : {symm (proj_le_pr1 H)})
+
+theorem proj_congr {a b : ℕ × ℕ} (H : rel a b) : proj a = proj b :=
+have special : ∀a b, pr2 a ≤ pr1 a → rel a b → proj a = proj b, from
+  take a b,
+  assume H2 : pr2 a ≤ pr1 a,
+  assume H : rel a b,
+  have H3 : pr1 a + pr2 b ≤ pr2 a + pr1 b, from subst H (le_refl (pr1 a + pr2 b)),
+  have H4 : pr2 b ≤ pr1 b, from add_le_inv H3 H2,
+  have H5 : pr1 (proj a) = pr1 (proj b), from
+    calc
+      pr1 (proj a) = pr1 a - pr2 a : proj_ge_pr1 H2
+	... = pr1 a + pr2 b - pr2 b - pr2 a : {symm (sub_add_left (pr1 a) (pr2 b))}
+	... = pr2 a + pr1 b - pr2 b - pr2 a : {H}
+	... = pr2 a + pr1 b - pr2 a - pr2 b : {sub_comm _ _ _}
+	... = pr1 b - pr2 b : {sub_add_left2 (pr2 a) (pr1 b)}
+	... = pr1 (proj b) : symm (proj_ge_pr1 H4),
+  have H6 : pr2 (proj a) = pr2 (proj b), from
+    calc
+      pr2 (proj a) = 0 : proj_ge_pr2 H2
+	... = pr2 (proj b) : {symm (proj_ge_pr2 H4)},
+  prod_eq H5 H6,
+or_elim (le_total (pr2 a) (pr1 a))
+  (assume H2 : pr2 a ≤ pr1 a, special a b H2 H)
+  (assume H2 : pr1 a ≤ pr2 a,
+    have H3 : pr2 (flip a) ≤ pr1 (flip a), from P_flip H2,
+    have H4 : proj (flip a) = proj (flip b), from special (flip a) (flip b) H3 (rel_flip H),
+    have H5 : flip (proj a) = flip (proj b), from subst (proj_flip a) (subst (proj_flip b) H4),
+    show proj a = proj b, from flip_inj H5)
+
+theorem proj_inj {a b : ℕ × ℕ} (H : proj a = proj b) : rel a b :=
+representative_map_equiv_inj rel_equiv proj_rel @proj_congr H
+
+theorem proj_zero_or (a : ℕ × ℕ) : pr1 (proj a) = 0 ∨ pr2 (proj a) = 0 :=
+or_elim (le_total (pr2 a) (pr1 a))
+  (assume H : pr2 a ≤ pr1 a, or_intro_right _ (proj_ge_pr2 H))
+  (assume H : pr1 a ≤ pr2 a, or_intro_left _ (proj_le_pr1 H))
+
+theorem proj_idempotent (a : ℕ × ℕ) : proj (proj a) = proj a :=
+representative_map_idempotent_equiv proj_rel @proj_congr a
+
+-- ## Definition of ℤ and basic theorems and definitions
+
+definition int := image proj
+notation `ℤ`:max := int
+
+definition psub : ℕ × ℕ → ℤ := fun_image proj
+definition rep : ℤ → ℕ × ℕ := subtype.elt_of
+
+theorem quotient : is_quotient rel psub rep :=
+representative_map_to_quotient_equiv rel_equiv proj_rel @proj_congr
+
+theorem psub_rep (a : ℤ) : psub (rep a) = a :=
+abs_rep quotient a
+
+theorem destruct (a : ℤ) : ∃n m : ℕ, a = psub (pair n m) :=
+exists_intro (pr1 (rep a))
+  (exists_intro (pr2 (rep a))
+    (calc
+      a = psub (rep a) : symm (psub_rep a)
+    ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {symm (prod_ext (rep a))}))
+
+definition of_nat (n : ℕ) : ℤ := psub (pair n 0)
+
+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 :=
+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
+
+--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
+    ... = n : by simp
+
+theorem of_nat_inj {n m : ℕ} (H : of_nat n = of_nat m) : n = m :=
+calc
+  n = to_nat (of_nat n) : symm (to_nat_of_nat n)
+    ... = to_nat (of_nat m) : {H}
+    ... = m : to_nat_of_nat m
+
+theorem abs_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
+    dist xa ya = (to_nat (psub (pair xa ya))) : by simp
+      ... = (to_nat a) : {symm Ha}
+      ... = 0 : H,
+have H3 : xa = ya, from dist_eq_zero H2,
+calc
+  a = psub (pair xa ya) : Ha
+... = psub (pair ya ya) : {H3}
+... = 0 : eq_zero_intro ya
+
+-- add_rewrite abs_of_nat
+
+-- ## neg
+
+
+definition neg : ℤ → ℤ := quotient_map quotient flip
+
+-- TODO: is this good?
+prefix `-`:80 := neg
+
+theorem neg_comp (n m : ℕ) : -psub (pair n m) = psub (pair m n) :=
+have H : ∀a, -psub a = psub (flip a),
+  from take a, comp_quotient_map quotient @rel_flip (rel_refl _),
+calc
+  -psub (pair n m) = psub (flip (pair n m)) : H (pair n m)
+    ... = psub (pair m n) : by simp
+
+-- add_rewrite neg_comp --local
+
+theorem neg_zero : -0 = 0 :=
+calc -psub (pair 0 0) = psub (pair 0 0) : neg_comp 0 0
+
+theorem neg_neg (a : ℤ) : -(-a) = a :=
+obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a,
+by simp
+
+-- add_rewrite neg_neg neg_zero
+
+theorem neg_inj {a b : ℤ} (H : -a = -b) : a = b :=
+(by simp) ◂ congr_arg neg H
+
+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) :=
+obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a,
+by simp
+
+theorem pos_eq_neg {n m : ℕ} (H : n = -m) : n = 0 ∧ m = 0 :=
+have H2 : ∀n : ℕ, n = psub (pair n 0), from take n : ℕ, refl (n),
+have H3 : psub (pair n 0) = psub (pair 0 m), from (by simp) ◂ H,
+have H4 : rel (pair n 0) (pair 0 m), from R_intro_refl quotient rel_refl H3,
+have H5 : n + m = 0, from
+  calc
+    n + m = pr1 (pair n 0) + pr2 (pair 0 m) : by simp
+      ... = pr2 (pair n 0) + pr1 (pair 0 m) : H4
+      ... = 0 : by simp,
+ add_eq_zero H5
+
+-- add_rewrite abs_neg
+
+---reverse equalities
+
+opaque_hint (exposing int)
+
+theorem cases (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - n) :=
+have Hrep : proj (rep a) = rep a, from @idempotent_image_fix _ proj proj_idempotent a,
+or_imp_or (or_swap (proj_zero_or (rep a)))
+  (assume H : pr2 (proj (rep a)) = 0,
+    have H2 : pr2 (rep a) = 0, from subst Hrep H,
+    exists_intro (pr1 (rep a))
+      (calc
+	a = psub (rep a) : symm (psub_rep a)
+	  ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {symm (prod_ext (rep a))}
+	  ... = psub (pair (pr1 (rep a)) 0) : {H2}
+	  ... = of_nat (pr1 (rep a)) : refl _))
+  (assume H : pr1 (proj (rep a)) = 0,
+    have H2 : pr1 (rep a) = 0, from subst Hrep H,
+    exists_intro (pr2 (rep a))
+      (calc
+	a = psub (rep a) : symm (psub_rep a)
+	  ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {symm (prod_ext (rep a))}
+	  ... = psub (pair 0 (pr2 (rep a))) : {H2}
+	  ... = -psub (pair (pr2 (rep a)) 0) : by simp
+	  ... = -of_nat (pr2 (rep a)) : refl _))
+
+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 :=
+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))
+
+---reverse equalities, rename
+theorem cases_succ (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - of_nat (succ n)) :=
+or_elim (cases a)
+  (assume H : (∃n : ℕ, a = of_nat n), or_intro_left _ H)
+  (assume H,
+    obtain (n : ℕ) (H2 : a = -of_nat n), from H,
+    discriminate
+      (assume H3 : n = 0,
+	have H4 : a = of_nat 0, from
+	  calc
+	    a = - of_nat n : H2
+	  ... = - of_nat 0 : {H3}
+	  ... = of_nat 0 : neg_zero,
+	or_intro_left _ (exists_intro 0 H4))
+      (take k : ℕ,
+	assume H3 : n = succ k,
+	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 :=
+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))
+
+theorem of_nat_eq_neg_of_nat {n m : ℕ} (H : n = - m) : n = 0 ∧ m = 0 :=
+have H2 : n = psub (pair 0 m), from
+  calc
+    n = -m : H
+      ... = -psub (pair m 0) : refl (-m)
+      ... = psub (pair 0 m) : by simp,
+have H3 : rel (pair n 0) (pair 0 m), from R_intro_refl quotient rel_refl H2,
+have H4 : n + m = 0, from
+  calc
+    n + m = pr1 (pair n 0) + pr2 (pair 0 m) : by simp
+      ... = pr2 (pair n 0) + pr1 (pair 0 m) : H3
+      ... = 0 : by simp,
+add_eq_zero H4
+
+--some of these had to be transparent for theorem cases
+opaque_hint (hiding psub proj)
+
+-- ## add
+
+theorem rel_add {a a' b b' : ℕ × ℕ} (Ha : rel a a') (Hb : rel b b')
+  : rel (map_pair2 add a b) (map_pair2 add a' b') :=
+calc
+  pr1 (map_pair2 add a b) + pr2 (map_pair2 add a' b')  = pr1 a + pr2 a' + (pr1 b + pr2 b') : by simp
+    ... = pr2 a + pr1 a' + (pr1 b + pr2 b') : {Ha}
+    ... = pr2 a + pr1 a' + (pr2 b + pr1 b') : {Hb}
+    ... = pr2 (map_pair2 add a b) + pr1 (map_pair2 add a' b') : by simp
+
+definition add : ℤ → ℤ → ℤ := quotient_map_binary quotient (map_pair2 nat.add)
+infixl `+` := int.add
+
+theorem add_comp (n m k l : ℕ) : psub (pair n m) + psub (pair k l) = psub (pair (n + k) (m + l)) :=
+have H : ∀a b, psub a + psub b = psub (map_pair2 nat.add a b),
+  from comp_quotient_map_binary_refl rel_refl quotient @rel_add,
+trans (H (pair n m) (pair k l)) (by simp)
+
+-- add_rewrite add_comp --local
+
+theorem add_comm (a b : ℤ) : a + b = b + a :=
+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 add_assoc (a b c : ℤ) : a + b + c = a + (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 add_left_comm (a b c : ℤ) : a + (b + c) = b + (a + c) :=
+left_comm add_comm add_assoc a b c
+
+theorem add_right_comm (a b c : ℤ) : a + b + c = a + c + b :=
+right_comm add_comm add_assoc a b c
+
+-- ### interaction of add with other functions and constants
+
+theorem add_zero_right (a : ℤ) : a + 0 = a :=
+obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a,
+have H0 : 0 = psub (pair 0 0), from refl 0,
+by simp
+
+theorem add_zero_left (a : ℤ) : 0 + a = a :=
+subst (add_comm a 0) (add_zero_right a)
+
+theorem add_inverse_right (a : ℤ) : a + -a = 0 :=
+have H : ∀n, psub (pair n n) = 0, from eq_zero_intro,
+obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a,
+by simp
+
+theorem add_inverse_left (a : ℤ) : -a + a = 0 :=
+subst (add_comm a (-a)) (add_inverse_right a)
+
+theorem neg_add_distr (a b : ℤ) : -(a + b) = -a + -b :=
+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::≤
+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,
+  from dist_add_le_add_dist xa xb ya yb,
+by simp
+
+-- TODO: add this to eq
+-- notation A `=` B `:` C := @eq C A B
+
+-- TODO: note, we have to add #nat to get the right interpretation
+theorem add_of_nat (n m : nat) : of_nat n + of_nat m = #nat n + m := -- this is of_nat (n + m)
+have H : ∀n : ℕ, n = psub (pair n 0), from take n : ℕ, refl n,
+by simp
+
+-- add_rewrite add_of_nat
+
+theorem of_nat_succ (n : ℕ) : of_nat (succ n) = of_nat n + 1 :=
+by simp
+
+-- ## sub
+definition sub (a b : ℤ) : ℤ := a + -b
+infixl `-`:65 := int.sub
+
+theorem sub_def (a b : ℤ) : a - b = a + -b :=
+refl (a - b)
+
+theorem add_neg_right (a b : ℤ) : a + -b = a - b :=
+refl (a - b)
+
+theorem add_neg_left (a b : ℤ) : -a + b = b - a :=
+add_comm (-a) b
+
+-- opaque_hint (hiding int.sub)
+
+-- TODO: why doesn't the shorter proof work?
+theorem sub_neg_right (a b : ℤ) : a - (-b) = a + b :=
+calc
+   a - (-b) = a + (- (- b)) : rfl
+     ... = a + b : {neg_neg b}
+-- subst (neg_neg b) (refl (a - (-b))) 
+
+theorem sub_neg_neg (a b : ℤ) : -a - (-b) = b - a :=
+subst (neg_neg b) (add_comm (-a) (-(-b)))
+
+theorem sub_self (a : ℤ) : a - a = 0 :=
+add_inverse_right a
+
+theorem sub_zero_right (a : ℤ) : a - 0 = a :=
+subst (symm neg_zero) (add_zero_right a) 
+
+theorem sub_zero_left (a : ℤ) : 0 - a = -a :=
+add_zero_left (-a)
+
+theorem neg_sub  (a b : ℤ) : -(a - b) = -a + b :=
+calc
+  -(a - b) = -a + -(-b) : neg_add_distr a (-b)
+    ... = -a + b : {neg_neg b}
+
+theorem neg_sub_flip (a b : ℤ) : -(a - b) = b - a :=
+calc
+  -(a - b) = -a + b : neg_sub a b
+    ... = b - a : add_comm (-a) b
+
+theorem sub_sub_assoc (a b c : ℤ) : a - b - c = a - (b + c) :=
+calc
+  a - b - c = a + (-b + -c) : add_assoc a (-b) (-c)
+    ... = a + -(b + c) : {symm (neg_add_distr b c)}
+
+theorem sub_add_assoc (a b c : ℤ) : a - b + c = a - (b - c) :=
+calc
+  a - b + c = a + (-b + c) : add_assoc a (-b) c
+    ... = a + -(b - c) : {symm (neg_sub b c)}
+
+theorem add_sub_assoc (a b c : ℤ) : a + b - c = a + (b - c) :=
+add_assoc a b (-c)
+
+theorem add_sub_inverse (a b : ℤ) : a + b - b = a :=
+calc
+  a + b - b = a + (b - b) : add_assoc a b (-b)
+    ... = a + 0 : {sub_self b}
+    ... = a : add_zero_right a
+
+theorem add_sub_inverse2 (a b : ℤ) : a + b - a = b :=
+subst (add_comm b a) (add_sub_inverse b a) 
+
+theorem sub_add_inverse (a b : ℤ) : a - b + b = a :=
+subst (add_right_comm a b (-b)) (add_sub_inverse a b) 
+
+-- add_rewrite add_zero_left add_zero_right
+-- add_rewrite add_comm add_assoc add_left_comm
+-- add_rewrite sub_def add_inverse_right add_inverse_left
+-- add_rewrite neg_add_distr
+---- add_rewrite sub_sub_assoc sub_add_assoc add_sub_assoc
+---- add_rewrite add_neg_right add_neg_left
+---- add_rewrite sub_self
+
+-- ### inversion theorems for add and sub
+
+-- a + a = 0 -> a = 0
+-- a = -a -> a = 0
+
+theorem add_cancel_right {a b c : ℤ} (H : a + c = b + c) : a = b :=
+calc
+  a = a + c - c : symm (add_sub_inverse a c)
+... = b + c - c : {H}
+... = b : add_sub_inverse b c
+
+theorem add_cancel_left {a b c : ℤ} (H : a + b = a + c) : b = c :=
+add_cancel_right (subst (subst H (add_comm a b)) (add_comm a c))
+
+theorem add_eq_zero_right {a b : ℤ} (H : a + b = 0) : -a = b :=
+have H2 : a + -a = a + b, from subst (symm (add_inverse_right a)) (symm H),
+show -a = b, from add_cancel_left H2
+
+theorem add_eq_zero_left {a b : ℤ} (H : a + b = 0) : -b = a :=
+neg_move (add_eq_zero_right H)
+
+theorem add_eq_self {a b : ℤ} (H : a + b = a) : b = 0 :=
+add_cancel_left (trans H (symm (add_zero_right a)))
+
+theorem sub_inj_left {a b c : ℤ} (H : a - b = a - c) : b = c :=
+neg_inj (add_cancel_left H)
+
+theorem sub_inj_right {a b c : ℤ} (H : a - b = c - b) : a = c :=
+add_cancel_right H
+
+theorem sub_eq_zero {a b : ℤ} (H : a - b = 0) : a = b :=
+neg_inj (add_eq_zero_right H)
+
+theorem add_imp_sub_right {a b c : ℤ} (H : a + b = c) : c - b = a :=
+have H2 : c - b + b = a + b, from trans (sub_add_inverse c b) (symm H),
+add_cancel_right H2
+
+theorem add_imp_sub_left {a b c : ℤ} (H : a + b = c) : c - a = b :=
+add_imp_sub_right (subst (add_comm a b) H)
+
+theorem sub_imp_add {a b c : ℤ} (H : a - b = c) : c + b = a :=
+let H' := add_imp_sub_right H in
+subst (neg_neg b) H'
+-- TODO: again, this doesn't work
+-- subst (neg_neg b) (add_imp_sub_right H)
+-- In fact, add [inline] to the definition above and it breaks!
+
+theorem sub_imp_sub {a b c : ℤ} (H : a - b = c) : a - c = b :=
+have H2 : c + b = a, from sub_imp_add H, add_imp_sub_left H2
+
+theorem sub_add_add_right (a b c : ℤ) : a + c - (b + c) = a - b :=
+calc
+  a + c - (b + c) = a + (c - (b + c)) : add_sub_assoc a c (b + c)
+    ... = a + (c - b - c) : {symm (sub_sub_assoc c b c)}
+    ... = a + -b : {add_sub_inverse2 c (-b)}
+
+theorem sub_add_add_left (a b c : ℤ) : c + a - (c + b) = a - b :=
+subst (add_comm b c) (subst (add_comm a c) (sub_add_add_right a b c))
+
+-- TODO: fix this
+theorem dist_def (n m : ℕ) : dist n m = (to_nat (of_nat n - m)) :=
+have H [fact] : of_nat n - m = psub (pair n m), from
+  calc
+    psub (pair n 0) + -psub (pair m 0) = psub (pair (n + 0) (0 + m)) : by simp
+      ... = psub (pair n m) : by simp,
+calc
+  dist n m = (to_nat (psub (pair n m))) : by simp
+    ... = (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
+  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,
+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))
+	(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))
+  + pr2 (pair (pr1 u' * pr1 v' + pr2 u' * pr2 v') (pr1 u' * pr2 v' + pr2 u' * pr1 v'))
+  = (pr1 u * pr1 v + pr2 u * pr2 v) + (pr1 u' * pr2 v' + pr2 u' * pr1 v') : by simp
+... = (pr1 u * pr2 v + pr2 u * pr1 v) + (pr1 u' * pr1 v' + pr2 u' * pr2 v') : rel_mul_prep H1 H2
+... = pr2 (pair (pr1 u * pr1 v + pr2 u * pr2 v) (pr1 u * pr2 v + pr2 u * pr1 v))
+  + pr1 (pair (pr1 u' * pr1 v' + pr2 u' * pr2 v') (pr1 u' * pr2 v' + pr2 u' * pr1 v')) : by simp
+
+definition mul : ℤ → ℤ → ℤ := quotient_map_binary quotient
+  (fun u v : ℕ × ℕ, pair (pr1 u * pr1 v + pr2 u * pr2 v) (pr1 u * pr2 v + pr2 u * pr1 v))
+
+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)) :=
+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,
+trans (H (pair n m) (pair k l)) (by simp)
+
+-- add_rewrite mul_comp
+
+theorem mul_comm (a b : ℤ) : a * b = b * a :=
+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 mul_assoc (a b c : ℤ) : (a * b) * c = a * (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_left_comm : ∀a b c : ℤ, a * (b * c) = b * (a * c) :=
+left_comm mul_comm mul_assoc
+
+theorem mul_right_comm : ∀a b c : ℤ, a * b * c = a * c * b :=
+right_comm mul_comm mul_assoc
+
+-- ### interaction with other objects
+
+theorem mul_zero_right (a : ℤ) : a * 0 = 0 :=
+obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a,
+have H0 : 0 = psub (pair 0 0), from refl 0,
+by simp
+
+theorem mul_zero_left (a : ℤ) : 0 * a = 0 :=
+subst (mul_comm a 0) (mul_zero_right a) 
+
+theorem mul_one_right (a : ℤ) : a * 1 = a :=
+obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a,
+have H1 : 1 = psub (pair 1 0), from refl 1,
+by simp
+
+theorem mul_one_left (a : ℤ) : 1 * a = a :=
+subst (mul_comm a 1) (mul_one_right a) 
+
+theorem mul_neg_right (a b : ℤ) : a * -b = -(a * b) :=
+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 mul_neg_left (a b : ℤ) : -a * b = -(a * b) :=
+subst (mul_comm b a) (subst (mul_comm b (-a)) (mul_neg_right b a))
+
+-- add_rewrite mul_neg_right mul_neg_left
+
+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 :=
+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 :=
+calc
+  a * (b + c) = (b + c) * a : mul_comm a (b + c)
+    ... = b * a + c * a : mul_distr_right 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 :=
+calc
+  (a + -b) * c = a * c + -b * c : mul_distr_right 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 :=
+calc
+  a * (b + -c) = a * b + a * -c : mul_distr_left 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 :=
+have H : ∀n : ℕ, n = psub (pair n 0), from take n : ℕ, refl n,
+by simp
+
+theorem mul_to_nat (a b : ℤ) : (to_nat (a * b)) = #nat (to_nat a) * (to_nat b) :=
+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 ya * dist xb yb = dist (xa * xb + ya * yb) (xa * yb + ya * xb),
+  from dist_mul_dist xa ya xb yb,
+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
+
+
+-- ---------- inversion
+
+theorem mul_eq_zero {a b : ℤ} (H : a * b = 0) : a = 0 ∨ b = 0 :=
+have H2 : (to_nat a) * (to_nat b) = 0, from
+  calc
+    (to_nat a) * (to_nat b) = (to_nat (a * b)) : symm (mul_to_nat a b)
+      ... = (to_nat 0) : {H}
+      ... = 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)
+
+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,
+have H3 : a = 0 ∨ b - c = 0, from mul_eq_zero H2,
+or_imp_or_right H3 (assume H4 : b - c = 0, sub_eq_zero H4)
+
+theorem mul_cancel_left {a b c : ℤ} (H1 : a ≠ 0) (H2 : a * b = a * c) : b = c :=
+resolve_right (mul_cancel_left_or H2) H1
+
+theorem mul_cancel_right_or {a b c : ℤ} (H : b * a = c * a) : a = 0 ∨ b = c :=
+mul_cancel_left_or (subst (subst H (mul_comm b a)) (mul_comm c a))
+
+theorem mul_cancel_right {a b c : ℤ} (H1 : c ≠ 0) (H2 : a * c = b * c) : a = b :=
+resolve_right (mul_cancel_right_or H2) H1
+
+theorem mul_ne_zero {a b : ℤ} (Ha : a ≠ 0) (Hb : b ≠ 0) : a * b ≠ 0 :=
+not_intro
+  (assume H : a * b = 0,
+    or_elim (mul_eq_zero H)
+      (assume H2 : a = 0, absurd H2 Ha)
+      (assume H2 : b = 0, absurd H2 Hb))
+
+theorem mul_ne_zero_left {a b : ℤ} (H : a * b ≠ 0) : a ≠ 0 :=
+not_intro
+  (assume H2 : a = 0,
+    have H3 : a * b = 0, by simp,
+    absurd H3 H)
+
+theorem mul_ne_zero_right {a b : ℤ} (H : a * b ≠ 0) : b ≠ 0 :=
+mul_ne_zero_left (subst (mul_comm a b) H)
+
+-- ## le
+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
+
+theorem le_elim {a b : ℤ} (H : a ≤ b) : ∃n : ℕ, a + n = b :=
+H
+
+-- ### partial order
+
+theorem le_refl (a : ℤ) : a ≤ a :=
+le_intro (add_zero_right a)
+
+theorem le_of_nat (n m : ℕ) : (of_nat n ≤ of_nat m) ↔ (n ≤ m) :=
+iff_intro
+  (assume H : of_nat n ≤ of_nat m,
+    obtain (k : ℕ) (Hk : of_nat n + of_nat k = of_nat m), from le_elim H,
+    have H2 : n + k = m, from of_nat_inj (trans (symm (add_of_nat n k)) Hk),
+    nat.le_intro H2)
+  (assume H : n ≤ m,
+    obtain (k : ℕ) (Hk : n + k = m), from nat.le_elim H,
+    have H2 : of_nat n + of_nat k = of_nat m, from subst Hk (add_of_nat n k),
+    le_intro H2)
+
+theorem le_trans {a b c : ℤ} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c :=
+obtain (n : ℕ) (Hn : a + n = b), from le_elim H1,
+obtain (m : ℕ) (Hm : b + m = c), from le_elim H2,
+have H3 : a + of_nat (n + m) = c, from
+  calc
+    a + of_nat (n + m) = a + (of_nat n + m) : {symm (add_of_nat n m)}
+      ... = a + n + m : symm (add_assoc a n m)
+      ... = b + m : {Hn}
+      ... = c : Hm,
+le_intro H3
+
+theorem le_antisym {a b : ℤ} (H1 : a ≤ b) (H2 : b ≤ a) : a = b :=
+obtain (n : ℕ) (Hn : a + n = b), from le_elim H1,
+obtain (m : ℕ) (Hm : b + m = a), from le_elim H2,
+have H3 : a + of_nat (n + m) = a + 0, from
+  calc
+    a + of_nat (n + m) = a + (of_nat n + m) : {symm (add_of_nat n m)}
+      ... = a + n + m : symm (add_assoc a n m)
+      ... = b + m : {Hn}
+      ... = a : Hm
+      ... = a + 0 : symm (add_zero_right a),
+have H4 : of_nat (n + m) = of_nat 0, from add_cancel_left H3,
+have H5 : n + m = 0, from of_nat_inj H4,
+have H6 : n = 0, from nat.add_eq_zero_left H5,
+show a = b, from
+  calc
+    a = a + of_nat 0 : symm (add_zero_right a)
+      ... = a + n : {symm H6}
+      ... = b : Hn
+
+-- ### interaction with add
+
+theorem le_add_of_nat_right (a : ℤ) (n : ℕ) : a ≤ a + n :=
+le_intro (refl (a + n))
+
+theorem le_add_of_nat_left (a : ℤ) (n : ℕ) : a ≤ n + a :=
+le_intro (add_comm a n)
+
+theorem add_le_left {a b : ℤ} (H : a ≤ b) (c : ℤ) : c + a ≤ c + b :=
+obtain (n : ℕ) (Hn : a + n = b), from le_elim H,
+have H2 : c + a + n = c + b, from
+  calc
+    c + a + n = c + (a + n) : add_assoc c a n
+      ... = c + b : {Hn},
+le_intro H2
+
+theorem add_le_right {a b : ℤ} (H : a ≤ b) (c : ℤ) : a + c ≤ b + c :=
+subst (add_comm c b) (subst (add_comm c a) (add_le_left H c))
+
+theorem add_le {a b c d : ℤ} (H1 : a ≤ b) (H2 : c ≤ d) : a + c ≤ b + d :=
+le_trans (add_le_right H1 c) (add_le_left H2 b)
+
+theorem add_le_cancel_right {a b c : ℤ} (H : a + c ≤ b + c) : a ≤ b :=
+have H2 : a + c - c ≤ b + c - c, from add_le_right H (-c),
+subst (add_sub_inverse b c) (subst (add_sub_inverse a c) H2)
+
+theorem add_le_cancel_left {a b c : ℤ} (H : c + a ≤ c + b) : a ≤ b :=
+add_le_cancel_right (subst (add_comm c b) (subst (add_comm c a) H))
+
+theorem add_le_inv {a b c d : ℤ} (H1 : a + b ≤ c + d) (H2 : c ≤ a) : b ≤ d :=
+obtain (n : ℕ) (Hn : c + n = a), from le_elim H2,
+have H3 : c + (n + b) ≤ c + d, from subst (add_assoc c n b) (subst (symm Hn) H1),
+have H4 : n + b ≤ d, from add_le_cancel_left H3,
+show b ≤ d, from le_trans (le_add_of_nat_left b n) H4
+
+theorem le_add_of_nat_right_trans {a b : ℤ} (H : a ≤ b) (n : ℕ) : a ≤ b + n :=
+le_trans H (le_add_of_nat_right b n)
+
+theorem le_imp_succ_le_or_eq {a b : ℤ} (H : a ≤ b) : a + 1 ≤ b ∨ a = b :=
+obtain (n : ℕ) (Hn : a + n = b), from le_elim H,
+discriminate
+  (assume H2 : n = 0,
+    have H3 : a = b, from
+      calc
+	a = a + 0 : symm (add_zero_right a)
+	  ... = a + n : {symm H2}
+	  ... = b : Hn,
+    or_intro_right _ H3)
+  (take k : ℕ,
+    assume H2 : n = succ k,
+    have H3 : a + 1 + k = b, from
+      calc
+	a + 1 + k = a + succ k : by simp
+	  ... = a + n : by simp
+	  ... = b : Hn,
+    or_intro_left _ (le_intro H3))
+
+-- ### interaction with neg and sub
+
+theorem le_neg {a b : ℤ} (H : a ≤ b) : -b ≤ -a :=
+obtain (n : ℕ) (Hn : a + n = b), from le_elim H,
+have H2 : b - n = a, from add_imp_sub_right Hn,
+have H3 : -b + n = -a, from
+  calc
+    -b + n = -b + -(-n) : {symm (neg_neg n)}
+      ... = -(b - n) : symm (neg_add_distr b (-n))
+      ... = -a : {H2},
+le_intro H3
+
+theorem neg_le_zero {a : ℤ} (H : 0 ≤ a) : -a ≤ 0 :=
+subst neg_zero (le_neg H)
+
+theorem zero_le_neg {a : ℤ} (H : a ≤ 0) : 0 ≤ -a :=
+subst neg_zero (le_neg H)
+
+theorem le_neg_inv {a b : ℤ} (H : -a ≤ -b) : b ≤ a :=
+subst (neg_neg b) (subst (neg_neg a) (le_neg H))
+
+theorem le_sub_of_nat (a : ℤ) (n : ℕ) : a - n ≤ a :=
+le_intro (sub_add_inverse a n)
+
+theorem sub_le_right {a b : ℤ} (H : a ≤ b) (c : ℤ) : a - c ≤ b - c :=
+add_le_right H (-c)
+
+theorem sub_le_left {a b : ℤ} (H : a ≤ b) (c : ℤ) : c - b ≤ c - a :=
+add_le_left (le_neg H) c
+
+theorem sub_le {a b c d : ℤ} (H1 : a ≤ b) (H2 : d ≤ c) : a - c ≤ b - d :=
+add_le H1 (le_neg H2)
+
+theorem sub_le_right_inv {a b c : ℤ} (H : a - c ≤ b - c) : a ≤ b :=
+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)
+
+-- Less than, Greater than, Greater than or equal
+-- ----------------------------------------------
+
+definition lt (a b : ℤ) := a + 1 ≤ b
+infix `<` := int.lt
+
+definition ge (a b : ℤ) := b ≤ a
+infix `>=` := int.ge
+infix `≥`  := int.ge
+
+definition gt (a b : ℤ) := b < a
+infix `>` := int.gt
+
+theorem lt_def (a b : ℤ) : a < b ↔ a + 1 ≤ b :=
+iff_refl (a < b)
+
+theorem gt_def (n m : ℕ) : n > m ↔ m < n :=
+iff_refl (n > m)
+
+theorem ge_def (n m : ℕ) : n ≥ m ↔ m ≤ n :=
+iff_refl (n ≥ m)
+
+-- add_rewrite gt_def ge_def --it might be possible to remove this in Lean 0.2
+
+theorem lt_add_succ (a : ℤ) (n : ℕ) : a < a + succ n :=
+le_intro (show a + 1 + n = a + succ n, by simp)
+
+theorem lt_intro {a b : ℤ} {n : ℕ} (H : a + succ n = b) : a < b :=
+subst H (lt_add_succ a n)
+
+theorem lt_elim {a b : ℤ} (H : a < b) : ∃n : ℕ, a + succ n = b :=
+obtain (n : ℕ) (Hn : a + 1 + n = b), from le_elim H,
+have H2 : a + succ n = b, from
+  calc
+    a + succ n = a + 1 + n : by simp
+      ... = b : Hn,
+exists_intro n H2
+
+-- -- ### basic facts
+
+theorem lt_irrefl (a : ℤ) : ¬ a < a :=
+not_intro
+  (assume H : a < a,
+    obtain (n : ℕ) (Hn : a + succ n = a), from lt_elim H,
+    have H2 : a + succ n = a + 0, from
+      calc
+	a + succ n = a : Hn
+	  ... = a + 0 : by simp,
+    have H3 : succ n = 0, from add_cancel_left H2,
+    have H4 : succ n = 0, from of_nat_inj H3,
+    absurd H4 (succ_ne_zero n))
+
+theorem lt_imp_ne {a b : ℤ} (H : a < b) : a ≠ b :=
+not_intro (assume H2 : a = b, absurd (subst H2 H) (lt_irrefl b))
+
+theorem lt_of_nat (n m : ℕ) : (of_nat n < of_nat m) ↔ (n < m) :=
+calc
+  (of_nat n + 1 ≤ of_nat m) ↔ (of_nat (succ n) ≤ of_nat m) : by simp
+    ... ↔ (succ n ≤ m) : le_of_nat (succ n) m
+    ... ↔ (n < m) : iff_symm (eq_to_iff (nat.lt_def n m))
+
+theorem gt_of_nat (n m : ℕ) : (of_nat n > of_nat m) ↔ (n > m) :=
+lt_of_nat m n
+
+-- ### interaction with le
+
+theorem lt_imp_le_succ {a b : ℤ} (H : a < b) : a + 1 ≤ b :=
+H
+
+theorem le_succ_imp_lt {a b : ℤ} (H : a + 1 ≤ b) : a < b :=
+H
+
+theorem self_lt_succ (a : ℤ) : a < a + 1 :=
+le_refl (a + 1)
+
+theorem lt_imp_le {a b : ℤ} (H : a < b) : a ≤ b :=
+obtain (n : ℕ) (Hn : a + succ n = b), from lt_elim H,
+le_intro Hn
+
+theorem le_imp_lt_or_eq {a b : ℤ} (H : a ≤ b) : a < b ∨ a = b :=
+le_imp_succ_le_or_eq H
+
+theorem le_ne_imp_lt {a b : ℤ} (H1 : a ≤ b)  (H2 : a ≠ b) : a < b :=
+resolve_left (le_imp_lt_or_eq H1) H2
+
+theorem le_imp_lt_succ {a b : ℤ} (H : a ≤ b) : a < b + 1 :=
+add_le_right H 1
+
+theorem lt_succ_imp_le {a b : ℤ} (H : a < b + 1) : a ≤ b :=
+add_le_cancel_right H
+
+
+-- ### transitivity, antisymmmetry
+
+theorem lt_le_trans {a b c : ℤ} (H1 : a < b) (H2 : b ≤ c) : a < c :=
+le_trans H1 H2
+
+theorem le_lt_trans {a b c : ℤ} (H1 : a ≤ b) (H2 : b < c) : a < c :=
+le_trans (add_le_right H1 1) H2
+
+theorem lt_trans {a b c : ℤ} (H1 : a < b) (H2 : b < c) : a < c :=
+lt_le_trans H1 (lt_imp_le H2)
+
+theorem le_imp_not_gt {a b : ℤ} (H : a ≤ b) : ¬ a > b :=
+not_intro (assume H2 : a > b, absurd (le_lt_trans H H2) (lt_irrefl a))
+
+theorem lt_imp_not_ge {a b : ℤ} (H : a < b) : ¬ a ≥ b :=
+not_intro (assume H2 : a ≥ b, absurd (lt_le_trans H H2) (lt_irrefl a))
+
+theorem lt_antisym {a b : ℤ} (H : a < b) : ¬ b < a :=
+le_imp_not_gt (lt_imp_le H)
+
+-- ### interaction with addition
+
+-- TODO: can we get rid of "int."?
+theorem add_lt_left {a b : ℤ} (H : a < b) (c : ℤ) : c + a < c + b :=
+subst (symm (add_assoc c a 1)) (int.add_le_left H c)
+-- old proof
+-- substp (fun x, x ≤ c + b) (add_le_left H c) (symm (add_assoc c a 1))
+
+theorem add_lt_right {a b : ℤ} (H : a < b) (c : ℤ) : a + c < b + c :=
+subst (add_comm c b) (subst (add_comm c a) (add_lt_left H c))
+
+theorem add_le_lt {a b c d : ℤ} (H1 : a ≤ c) (H2 : b < d) : a + b < c + d :=
+le_lt_trans (add_le_right H1 b) (add_lt_left H2 c)
+
+theorem add_lt_le {a b c d : ℤ} (H1 : a < c) (H2 : b ≤ d) : a + b < c + d :=
+lt_le_trans (add_lt_right H1 b) (add_le_left H2 c)
+
+theorem add_lt {a b c d : ℤ} (H1 : a < c) (H2 : b < d) : a + b < c + d :=
+add_lt_le H1 (lt_imp_le H2)
+
+theorem add_lt_cancel_left {a b c : ℤ} (H : c + a < c + b) : a < b :=
+add_le_cancel_left (subst (add_assoc c a 1) (show c + a + 1 ≤ c + b, from H))
+
+theorem add_lt_cancel_right {a b c : ℤ} (H : a + c < b + c) : a < b :=
+add_lt_cancel_left (subst (add_comm b c) (subst (add_comm a c) H))
+
+
+-- ### interaction with neg and sub
+
+theorem lt_neg {a b : ℤ} (H : a < b) : -b < -a :=
+have H2 : -(a + 1) + 1 = -a, by simp,
+have H3 : -b ≤ -(a + 1), from le_neg H,
+have H4 : -b + 1 ≤ -(a + 1) + 1, from add_le_right H3 1,
+subst H2 H4
+
+theorem neg_lt_zero {a : ℤ} (H : 0 < a) : -a < 0 :=
+subst neg_zero (lt_neg H)
+
+theorem zero_lt_neg {a : ℤ} (H : a < 0) : 0 < -a :=
+subst neg_zero (lt_neg H)
+
+theorem lt_neg_inv {a b : ℤ} (H : -a < -b) : b < a :=
+subst (neg_neg b) (subst (neg_neg a) (lt_neg H))
+
+theorem lt_sub_of_nat_succ (a : ℤ) (n : ℕ) : a - succ n < a :=
+lt_intro (sub_add_inverse a (succ n))
+
+theorem sub_lt_right {a b : ℤ} (H : a < b) (c : ℤ) : a - c < b - c :=
+add_lt_right H (-c)
+
+theorem sub_lt_left {a b : ℤ} (H : a < b) (c : ℤ) : c - b < c - a :=
+add_lt_left (lt_neg H) c
+
+theorem sub_lt {a b c d : ℤ} (H1 : a < b) (H2 : d < c) : a - c < b - d :=
+add_lt H1 (lt_neg H2)
+
+theorem sub_lt_right_inv {a b c : ℤ} (H : a - c < b - c) : a < b :=
+add_lt_cancel_right H
+
+theorem sub_lt_left_inv {a b c : ℤ} (H : c - a < c - b) : b < a :=
+lt_neg_inv (add_lt_cancel_left H)
+
+-- ### totality of lt and le
+
+-- add_rewrite succ_pos zero_le --move some of these to nat.lean
+-- add_rewrite le_of_nat lt_of_nat gt_of_nat --remove gt_of_nat in Lean 0.2
+-- add_rewrite le_neg lt_neg neg_le_zero zero_le_neg zero_lt_neg neg_lt_zero
+
+-- axiom sorry {P : Prop} : P
+
+theorem neg_le_pos (n m : ℕ) : -n ≤ m :=
+have H1 : of_nat 0 ≤ of_nat m, by simp,
+have H2 : -n ≤ 0, by simp,
+le_trans H2 H1
+
+theorem le_or_gt (a b : ℤ) : a ≤ b ∨ a > b :=
+int_by_cases a
+  (take n : ℕ,
+    int_by_cases_succ b
+      (take m : ℕ,
+	show of_nat n ≤ m ∨ of_nat n > m, by simp) -- from (by simp) ◂ (le_or_gt n m))
+      (take m : ℕ,
+	show n ≤ -succ m ∨ n > -succ m, from
+	  have H0 : -succ m < -m, from lt_neg (subst (symm (of_nat_succ m)) (self_lt_succ m)),
+	  have H : -succ m < n, from lt_le_trans H0 (neg_le_pos m n),
+	  or_intro_right _ H))
+  (take n : ℕ,
+    int_by_cases_succ b
+      (take m : ℕ,
+	show -n ≤ m ∨ -n > m, from
+	  or_intro_left _ (neg_le_pos n m))
+      (take m : ℕ,
+	show -n ≤ -succ m ∨ -n > -succ m, from
+	  or_imp_or (le_or_gt (succ m) n)
+	    (assume H : succ m ≤ n,
+	      le_neg (iff_elim_left (iff_symm (le_of_nat (succ m) n)) H))
+	    (assume H : succ m > n,
+	      lt_neg (iff_elim_left (iff_symm (lt_of_nat n (succ m))) H))))
+
+theorem trichotomy_alt (a b : ℤ) : (a < b ∨ a = b) ∨ a > b :=
+or_imp_or_left (le_or_gt a b) (assume H : a ≤ b, le_imp_lt_or_eq H)
+
+theorem trichotomy (a b : ℤ) : a < b ∨ a = b ∨ a > b :=
+iff_elim_left (or_assoc _ _ _) (trichotomy_alt a b)
+
+theorem le_total (a b : ℤ) : a ≤ b ∨ b ≤ a :=
+or_imp_or_right (le_or_gt a b) (assume H : b < a, lt_imp_le H)
+
+theorem not_lt_imp_le {a b : ℤ} (H : ¬ a < b) : b ≤ a :=
+resolve_left (le_or_gt b a) H
+
+theorem not_le_imp_lt {a b : ℤ} (H : ¬ a ≤ b) : b < a :=
+resolve_right (le_or_gt a b) H
+
+-- (non)positivity and (non)negativity
+-- -------------------------------------
+
+-- ### basic
+
+-- see also "int_by_cases" and similar theorems
+
+theorem pos_imp_exists_nat {a : ℤ} (H : a ≥ 0) : ∃n : ℕ, a = n :=
+obtain (n : ℕ) (Hn : of_nat 0 + n = a), from le_elim H,
+exists_intro n (trans (symm Hn) (add_zero_left n))
+
+theorem neg_imp_exists_nat {a : ℤ} (H : a ≤ 0) : ∃n : ℕ, a = -n :=
+have H2 : -a ≥ 0, from zero_le_neg H,
+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 :=
+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 :=
+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}
+  ... = n : {to_nat_of_nat n}
+  ... = -a : symm (neg_move (symm Hn))
+
+theorem abs_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))))
+
+-- ### interaction of mul with le and lt
+
+theorem mul_le_left_nonneg {a b c : ℤ} (Ha : a ≥ 0) (H : b ≤ c) : a * b ≤ a * c :=
+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 + n) : by simp
+      ... = a * c : by simp,
+le_intro H2
+
+theorem mul_le_right_nonneg {a b c : ℤ} (Hb : b ≥ 0) (H : a ≤ c) : a * b ≤ c * b :=
+subst (mul_comm b c) (subst (mul_comm b a) (mul_le_left_nonneg Hb H))
+
+theorem mul_le_left_nonpos {a b c : ℤ} (Ha : a ≤ 0) (H : b ≤ c) : a * c ≤ a * b :=
+have H2 : -a * b ≤ -a * c, from mul_le_left_nonneg (zero_le_neg Ha) H,
+have H3 : -(a * b) ≤ -(a * c), from subst (mul_neg_left a c) (subst (mul_neg_left a b) H2),
+le_neg_inv H3
+
+theorem mul_le_right_nonpos {a b c : ℤ} (Hb : b ≤ 0) (H : c ≤ a) : a * b ≤ c * b :=
+subst (mul_comm b c) (subst (mul_comm b a) (mul_le_left_nonpos Hb H))
+
+---this theorem can be made more general by replacing either Ha with 0 ≤ a or Hb with 0 ≤ d...
+theorem mul_le_nonneg {a b c d : ℤ} (Ha : a ≥ 0) (Hb : b ≥ 0) (Hc : a ≤ c) (Hd : b ≤ d)
+  : a * b ≤ c * d :=
+le_trans (mul_le_right_nonneg Hb Hc) (mul_le_left_nonneg (le_trans Ha Hc) Hd)
+
+theorem mul_le_nonpos {a b c d : ℤ} (Ha : a ≤ 0) (Hb : b ≤ 0) (Hc : c ≤ a) (Hd : d ≤ b)
+  : a * b ≤ c * d :=
+le_trans (mul_le_right_nonpos Hb Hc) (mul_le_left_nonpos (le_trans Hc Ha) Hd)
+
+theorem mul_lt_left_pos {a b c : ℤ} (Ha : a > 0) (H : b < c) : a * b < a * c :=
+have H2 : a * b < a * b + a, from subst (add_zero_right (a * b)) (add_lt_left Ha (a * b)),
+have H3 : a * b + a ≤ a * c, from subst (by simp) (mul_le_left_nonneg (lt_imp_le Ha) H),
+lt_le_trans H2 H3
+
+theorem mul_lt_right_pos {a b c : ℤ} (Hb : b > 0) (H : a < c) : a * b < c * b :=
+subst (mul_comm b c) (subst (mul_comm b a) (mul_lt_left_pos Hb H))
+
+theorem mul_lt_left_neg {a b c : ℤ} (Ha : a < 0) (H : b < c) : a * c < a * b :=
+have H2 : -a * b < -a * c, from mul_lt_left_pos (zero_lt_neg Ha) H,
+have H3 : -(a * b) < -(a * c), from subst (mul_neg_left a c) (subst (mul_neg_left a b) H2),
+lt_neg_inv H3
+
+theorem mul_lt_right_neg {a b c : ℤ} (Hb : b < 0) (H : c < a) : a * b < c * b :=
+subst (mul_comm b c) (subst (mul_comm b a) (mul_lt_left_neg Hb H))
+
+theorem mul_le_lt_pos {a b c d : ℤ} (Ha : a > 0) (Hb : b ≥ 0) (Hc : a ≤ c) (Hd : b < d)
+  : a * b < c * d :=
+le_lt_trans (mul_le_right_nonneg Hb Hc) (mul_lt_left_pos (lt_le_trans Ha Hc) Hd)
+
+theorem mul_lt_le_pos {a b c d : ℤ} (Ha : a ≥ 0) (Hb : b > 0) (Hc : a < c) (Hd : b ≤ d)
+  : a * b < c * d :=
+lt_le_trans (mul_lt_right_pos Hb Hc) (mul_le_left_nonneg (le_trans Ha (lt_imp_le Hc)) Hd)
+
+theorem mul_lt_pos {a b c d : ℤ} (Ha : a > 0) (Hb : b > 0) (Hc : a < c) (Hd : b < d)
+  : a * b < c * d :=
+mul_lt_le_pos (lt_imp_le Ha) Hb Hc (lt_imp_le Hd)
+
+theorem mul_lt_neg {a b c d : ℤ} (Ha : a < 0) (Hb : b < 0) (Hc : c < a) (Hd : d < b)
+  : a * b < c * d :=
+lt_trans (mul_lt_right_neg Hb Hc) (mul_lt_left_neg (lt_trans Hc Ha) Hd)
+
+-- theorem mul_le_lt_neg and mul_lt_le_neg?
+
+theorem mul_lt_cancel_left_nonneg {a b c : ℤ} (Hc : c ≥ 0) (H : c * a < c * b) : a < b :=
+or_elim (le_or_gt b a)
+  (assume H2 : b ≤ a,
+    have H3 : c * b ≤ c * a, from mul_le_left_nonneg Hc H2,
+    absurd_elim _ H3 (lt_imp_not_ge H))
+  (assume H2 : a < b, H2)
+
+theorem mul_lt_cancel_right_nonneg {a b c : ℤ} (Hc : c ≥ 0) (H : a * c < b * c) : a < b :=
+mul_lt_cancel_left_nonneg Hc (subst (mul_comm b c) (subst (mul_comm a c) H))
+
+theorem mul_lt_cancel_left_nonpos {a b c : ℤ} (Hc : c ≤ 0) (H : c * b < c * a) : a < b :=
+have H2 : -(c * a) < -(c * b), from lt_neg H,
+have H3 : -c * a < -c * b,
+  from subst (symm (mul_neg_left c b)) (subst (symm (mul_neg_left c a)) H2),
+have H4 : -c ≥ 0, from zero_le_neg Hc,
+mul_lt_cancel_left_nonneg H4 H3
+
+theorem mul_lt_cancel_right_nonpos {a b c : ℤ} (Hc : c ≤ 0) (H : b * c < a * c) : a < b :=
+mul_lt_cancel_left_nonpos Hc (subst (mul_comm b c) (subst (mul_comm a c) H))
+
+theorem mul_le_cancel_left_pos {a b c : ℤ} (Hc : c > 0) (H : c * a ≤ c * b) : a ≤ b :=
+or_elim (le_or_gt a b)
+  (assume H2 : a ≤ b, H2)
+  (assume H2 : a > b,
+    have H3 : c * a > c * b, from mul_lt_left_pos Hc H2,
+    absurd_elim _ H3 (le_imp_not_gt H))
+
+theorem mul_le_cancel_right_pos {a b c : ℤ} (Hc : c > 0) (H : a * c ≤ b * c) : a ≤ b :=
+mul_le_cancel_left_pos Hc (subst (mul_comm b c) (subst (mul_comm a c) H))
+
+theorem mul_le_cancel_left_neg {a b c : ℤ} (Hc : c < 0) (H : c * b ≤ c * a) : a ≤ b :=
+have H2 : -(c * a) ≤ -(c * b), from le_neg H,
+have H3 : -c * a ≤ -c * b,
+  from subst (symm (mul_neg_left c b)) (subst (symm (mul_neg_left c a)) H2),
+have H4 : -c > 0, from zero_lt_neg Hc,
+mul_le_cancel_left_pos H4 H3
+
+theorem mul_le_cancel_right_neg {a b c : ℤ} (Hc : c < 0) (H : b * c ≤ a * c) : a ≤ b :=
+mul_le_cancel_left_neg Hc (subst (mul_comm b c) (subst (mul_comm a c) H))
+
+theorem mul_eq_one_left {a b : ℤ} (H : a * b = 1) : a = 1 ∨ a = - 1 :=
+have H2 : (to_nat a) * (to_nat b) = 1, from
+  calc
+    (to_nat a) * (to_nat b) = (to_nat (a * b)) : symm (mul_to_nat a b)
+      ... = (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)
+  (assume H4 : a = (to_nat a), subst H3 H4)
+  (assume H4 : a = - (to_nat a), subst H3 H4)
+
+theorem mul_eq_one_right {a b : ℤ} (H : a * b = 1) : b = 1 ∨ b = - 1 :=
+mul_eq_one_left (subst (mul_comm a b) H)
+
+
+-- sign function
+-- -------------
+
+definition sign (a : ℤ) : ℤ := if a > 0 then 1 else (if a < 0 then - 1 else 0)
+
+-- TODO: for kernel
+theorem or_elim3 {a b c d : Prop} (H : a ∨ b ∨ c) (Ha : a → d) (Hb : b → d) (Hc : c → d) : d :=
+or_elim H Ha (assume H2,or_elim H2 Hb Hc)
+
+theorem sign_pos {a : ℤ} (H : a > 0) : sign a = 1 :=
+if_pos H _ _
+
+theorem sign_negative {a : ℤ} (H : a < 0) : sign a = - 1 :=
+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
+
+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,
+have temp2 : ∀a : ℤ, a > 0 → a ≥ 0, from take a, lt_imp_le,
+or_elim3 (trichotomy a 0)
+  (assume H : a < 0, by simp)
+  (assume H : a = 0, by simp)
+  (assume H : a > 0, by simp)
+
+-- TODO: show decidable for equality (and avoid classical library)
+theorem sign_mul (a b : ℤ) : sign (a * b) = sign a * sign b :=
+or_elim (em (a = 0))
+  (assume Ha : a = 0, by simp)
+  (assume Ha : a ≠ 0,
+    or_elim (em (b = 0))
+      (assume Hb : b = 0, by simp)
+      (assume Hb : b ≠ 0,
+	have H : sign (a * b) * (to_nat (a * b)) = sign a * sign b  * (to_nat (a * b)), from
+	  calc
+	    sign (a * b) * (to_nat (a * b)) = a * b : mul_sign_to_nat (a * b)
+	      ... = sign a * (to_nat a) * b : {symm (mul_sign_to_nat a)}
+	      ... = 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'),
+	have H3 : (to_nat (a * b)) ≠ of_nat 0, from contrapos of_nat_inj H2,
+	mul_cancel_right H3 H))
+
+--set_option pp::coercion true
+
+theorem sign_idempotent (a : ℤ) : sign (sign a) = sign a :=
+have temp : of_nat 1 > 0, from iff_elim_left (iff_symm (lt_of_nat 0 1)) (succ_pos 0),
+    --this should be done with simp
+or_elim3 (trichotomy a 0) sorry sorry sorry
+--  (by simp)
+--  (by simp)
+--  (by simp)
+
+theorem sign_succ (n : ℕ) : sign (succ n) = 1 :=
+sign_pos (iff_elim_left (iff_symm (lt_of_nat 0 (succ n))) (succ_pos n)) 
+  --this should be done with simp
+
+theorem sign_neg (a : ℤ) : sign (-a) = - sign a :=
+have temp1 : a > 0 → -a < 0, from neg_lt_zero,
+have temp2 : a < 0 → -a > 0, from zero_lt_neg,
+or_elim3 (trichotomy a 0) sorry sorry sorry
+--  (by simp)
+--  (by simp)
+--  (by simp)
+
+-- add_rewrite sign_neg
+
+theorem abs_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)
+  sorry
+--  (by simp)
+
+theorem sign_to_nat (a : ℤ) : sign (to_nat a) = to_nat (sign a) :=
+have temp1 : ∀a : ℤ, a < 0 → a ≤ 0, from take a, lt_imp_le,
+have temp2 : ∀a : ℤ, a > 0 → a ≥ 0, from take a, lt_imp_le,
+or_elim3 (trichotomy a 0) sorry sorry sorry
+--  (by simp)
+--  (by simp)
+--  (by simp)
+
+
+-- set_opaque rel true
+-- set_opaque rep true
+-- set_opaque of_nat true
+-- set_opaque to_nat true
+-- set_opaque neg true
+-- set_opaque add true
+-- set_opaque mul true
+-- set_opaque le true
+-- set_opaque lt true
+-- set_opaque sign true
+--transparent: sub ge gt
+
+end int -- namespace int
diff --git a/library/standard/data/bool/default.lean b/library/standard/data/int/default.lean
similarity index 88%
rename from library/standard/data/bool/default.lean
rename to library/standard/data/int/default.lean
index d637c98d4..09e23846e 100644
--- a/library/standard/data/bool/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 .type .basic
+import data.nat.basic
diff --git a/library/standard/data/int/int.default b/library/standard/data/int/int.default
new file mode 100644
index 000000000..1e1a70042
--- /dev/null
+++ b/library/standard/data/int/int.default
@@ -0,0 +1,5 @@
+--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+--- Released under Apache 2.0 license as described in the file LICENSE.
+--- Author: Jeremy Avigad
+
+import .basic
\ No newline at end of file
diff --git a/library/standard/data/int/int.md b/library/standard/data/int/int.md
new file mode 100644
index 000000000..979518ab0
--- /dev/null
+++ b/library/standard/data/int/int.md
@@ -0,0 +1,6 @@
+data.int
+========
+
+The integers.
+
+* [basic](basic.lean) : the integers, with basic operations and order.
diff --git a/library/standard/data/list/basic.lean b/library/standard/data/list/basic.lean
index f4e2c806a..7a87c4b74 100644
--- a/library/standard/data/list/basic.lean
+++ b/library/standard/data/list/basic.lean
@@ -15,7 +15,7 @@ import logic
 -- import if -- for find
 
 using nat
-using eq_proofs
+using eq_ops
 
 namespace list
 
diff --git a/library/standard/data/nat/basic.lean b/library/standard/data/nat/basic.lean
index e9c9eb191..fdd36a578 100644
--- a/library/standard/data/nat/basic.lean
+++ b/library/standard/data/nat/basic.lean
@@ -1,12 +1,11 @@
-----------------------------------------------------------------------------------------------------
 --- Copyright (c) 2014 Floris van Doorn. All rights reserved.
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Floris van Doorn
-----------------------------------------------------------------------------------------------------
 
 import logic data.num tools.tactic struc.binary
-using num tactic binary eq_proofs
+using num tactic binary eq_ops
 using decidable (hiding induction_on rec_on)
+using relation -- for subst_iff
 
 -- TODO: this should go in tools, I think
 namespace helper_tactics
@@ -29,7 +28,19 @@ inductive nat : Type :=
 | zero : nat
 | succ : nat → nat
 
-notation `ℕ` : max := nat
+notation `ℕ`:max := nat
+
+theorem nat_rec_zero {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) : nat_rec x f zero = x
+
+theorem nat_rec_succ {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) (n : ℕ) :
+  nat_rec x f (succ n) = f n (nat_rec x f n)
+
+theorem induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P zero) (H2 : ∀ (n : ℕ) (IH : P n), P (succ n)) :
+  P a :=
+nat_rec H1 H2 a
+
+definition rec_on {P : ℕ → Type} (n : ℕ) (H1 : P zero) (H2 : ∀m, P m → P (succ m)) : P n :=
+nat_rec H1 H2 n
 
 
 -- Coercion from num
@@ -42,30 +53,20 @@ definition to_nat [coercion] [inline] (n : num) : ℕ :=
 num_rec zero
     (λ n, pos_num_rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
 
-theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat_rec x f 0 = x
-
-theorem nat_rec_succ {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) (n : ℕ) :
-  nat_rec x f (succ n) = f n (nat_rec x f n)
-
-theorem induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : ∀ (n : ℕ) (IH : P n), P (succ n)) :
-  P a :=
-nat_rec H1 H2 a
-
-definition rec_on {P : ℕ → Type} (n : ℕ) (H1 : P 0) (H2 : ∀m, P m → P (succ m)) : P n :=
-nat_rec H1 H2 n
-
 
 -- Successor and predecessor
 -- -------------------------
 
+-- TODO: this looks like a calc bug -- calc is using subst for iff, instead of =
+calc_subst subst
 theorem succ_ne_zero (n : ℕ) : succ n ≠ 0 :=
 assume H : succ n = 0,
 have H2 : true = false, from
   let f [inline] := (nat_rec false (fun a b, true)) in
     calc
-      true = f (succ n) : _
+      true = f (succ n) : rfl
        ... = f 0        : {H}
-       ... = false      : _,
+       ... = false      : rfl,
 absurd H2 true_ne_false
 
 -- add_rewrite succ_ne_zero
@@ -82,7 +83,7 @@ theorem zero_or_succ_pred (n : ℕ) : n = 0 ∨ n = succ (pred n) :=
 induction_on n
   (or_inl (refl 0))
   (take m IH, or_inr
-    (show succ m = succ (pred (succ m)), from congr2 succ (pred_succ m⁻¹)))
+    (show succ m = succ (pred (succ m)), from congr_arg succ (pred_succ m⁻¹)))
 
 theorem zero_or_exists_succ (n : ℕ) : n = 0 ∨ ∃k, n = succ k :=
 or_imp_or (zero_or_succ_pred n) (assume H, H)
@@ -122,7 +123,7 @@ have general : ∀n, decidable (n = m), from
 	(λ (n' : ℕ) (iH2 : decidable (n' = succ m')),
 	  have d1 : decidable (n' = m'), from iH1 n',
 	  decidable.rec_on d1
-	    (assume Heq : n' = m', inl (congr2 succ Heq))
+	    (assume Heq : n' = m', inl (congr_arg succ Heq))
 	    (assume Hne : n' ≠ m',
 	      have H1 : succ n' ≠ succ m', from
 		assume Heq, absurd (succ_inj Heq) Hne,
@@ -415,4 +416,4 @@ discriminate
 -- add_rewrite mul_succ_left mul_succ_right
 -- add_rewrite mul_comm mul_assoc mul_left_comm
 -- add_rewrite mul_distr_right mul_distr_left
-end nat
\ No newline at end of file
+end nat
diff --git a/library/standard/data/nat/order.lean b/library/standard/data/nat/order.lean
index d6e81358f..0b146c34e 100644
--- a/library/standard/data/nat/order.lean
+++ b/library/standard/data/nat/order.lean
@@ -1,14 +1,12 @@
-----------------------------------------------------------------------------------------------------
 --- Copyright (c) 2014 Floris van Doorn. All rights reserved.
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Floris van Doorn
-----------------------------------------------------------------------------------------------------
 
 import .basic
-using nat eq_proofs tactic
+import tools.fake_simplifier
 
--- until we have the simplifier...
-definition simp : tactic := apply @sorry
+using nat eq_ops tactic
+using fake_simplifier
 
 -- TODO: move these to logic.connectives
 theorem or_imp_or_left {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) : c ∨ b :=
@@ -30,7 +28,6 @@ namespace nat
 definition le (n m : ℕ) : Prop := exists k : nat, n + k = m
 
 infix  `<=`:50 := le
-
 infix  `≤`:50  := le
 
 theorem le_intro {n m k : ℕ} (H : n + k = m) : n ≤ m :=
@@ -583,4 +580,4 @@ 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
\ No newline at end of file
+end nat
diff --git a/library/standard/data/nat/sub.lean b/library/standard/data/nat/sub.lean
index 04e1a29b1..ebd40a1f5 100644
--- a/library/standard/data/nat/sub.lean
+++ b/library/standard/data/nat/sub.lean
@@ -1,13 +1,15 @@
-----------------------------------------------------------------------------------------------------
 --- Copyright (c) 2014 Floris van Doorn. All rights reserved.
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Floris van Doorn
-----------------------------------------------------------------------------------------------------
 
 import data.nat.order
-using nat eq_proofs tactic
+import tools.fake_simplifier
+
+using nat eq_ops tactic
 using helper_tactics
 
+using fake_simplifier
+
 namespace nat
 
 -- data.nat.basic2
@@ -508,4 +510,4 @@ or_elim (le_total k l)
   (assume H : k ≤ l, dist_comm l k ▸ dist_comm _ _ ▸ aux l k H)
   (assume H : l ≤ k, aux k l H)
 
-end nat
\ No newline at end of file
+end nat
diff --git a/library/standard/data/num.lean b/library/standard/data/num.lean
index 527cb6334..d521551f5 100644
--- a/library/standard/data/num.lean
+++ b/library/standard/data/num.lean
@@ -21,9 +21,9 @@ inductive num : Type :=
 | pos   : pos_num → num
 
 theorem inhabited_pos_num [instance] : inhabited pos_num :=
-inhabited_intro one
+inhabited_mk one
 
 theorem inhabited_num [instance] : inhabited num :=
-inhabited_intro zero
+inhabited_mk zero
 
-end num
\ No newline at end of file
+end num
diff --git a/library/standard/data/option.lean b/library/standard/data/option.lean
index 43e650e25..484d9f3b2 100644
--- a/library/standard/data/option.lean
+++ b/library/standard/data/option.lean
@@ -4,7 +4,7 @@
 -- Author: Leonardo de Moura
 ----------------------------------------------------------------------------------------------------
 import logic.connectives.basic logic.connectives.eq logic.classes.inhabited logic.classes.decidable
-using eq_proofs decidable
+using eq_ops decidable
 
 namespace option
 inductive option (A : Type) : Type :=
@@ -32,10 +32,10 @@ assume H : none = some a, absurd
   (not_is_none_some a)
 
 theorem some_inj {A : Type} {a₁ a₂ : A} (H : some a₁ = some a₂) : a₁ = a₂ :=
-congr2 (option_rec a₁ (λ a, a)) H
+congr_arg (option_rec a₁ (λ a, a)) H
 
 theorem inhabited_option [instance] (A : Type) : inhabited (option A) :=
-inhabited_intro none
+inhabited_mk none
 
 theorem decidable_eq [instance] {A : Type} {H : ∀a₁ a₂ : A, decidable (a₁ = a₂)} (o₁ o₂ : option A) : decidable (o₁ = o₂) :=
 rec_on o₁
@@ -45,4 +45,4 @@ rec_on o₁
     (take a₂ : A, decidable.rec_on (H a₁ a₂)
       (assume Heq : a₁ = a₂, inl (Heq ▸ refl _))
       (assume Hne : a₁ ≠ a₂, inr (assume Hn : some a₁ = some a₂, absurd (some_inj Hn) Hne))))
-end option
\ No newline at end of file
+end option
diff --git a/library/standard/data/prod.lean b/library/standard/data/prod.lean
index dabaccda8..6be995d82 100644
--- a/library/standard/data/prod.lean
+++ b/library/standard/data/prod.lean
@@ -4,6 +4,8 @@
 
 import logic.classes.inhabited logic.connectives.eq
 
+using inhabited
+
 inductive prod (A B : Type) : Type :=
 | pair : A → B → prod A B
 
@@ -39,10 +41,10 @@ section
   pair_destruct p1 (take a1 b1, pair_destruct p2 (take a2 b2 H1 H2, pair_eq H1 H2))
 
   theorem prod_inhabited (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) :=
-  inhabited_elim H1 (λa, inhabited_elim H2 (λb, inhabited_intro (pair a b)))
+  inhabited_destruct H1 (λa, inhabited_destruct H2 (λb, inhabited_mk (pair a b)))
 
 end
 
 instance prod_inhabited
 
-end prod
\ No newline at end of file
+end prod
diff --git a/library/standard/data/quotient/aux.lean b/library/standard/data/quotient/aux.lean
new file mode 100644
index 000000000..7d467410c
--- /dev/null
+++ b/library/standard/data/quotient/aux.lean
@@ -0,0 +1,175 @@
+-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Floris van Doorn
+
+import logic ..prod struc.relation
+import tools.fake_simplifier
+
+using prod eq_ops
+using fake_simplifier
+
+-- TODO: calc bug -- remove
+calc_subst subst
+
+
+namespace quotient
+
+-- auxliary facts about products
+-- -----------------------------
+
+-- ### flip
+
+definition flip {A B : Type} (a : A × B) : B × A := pair (pr2 a) (pr1 a)
+
+theorem flip_def {A B : Type} (a : A × B) : flip a = pair (pr2 a) (pr1 a) := refl (flip a)
+
+theorem flip_pair {A B : Type} (a : A) (b : B) : flip (pair a b) = pair b a := rfl
+
+theorem flip_pr1 {A B : Type} (a : A × B) : pr1 (flip a) = pr2 a := rfl
+
+theorem flip_pr2 {A B : Type} (a : A × B) : pr2 (flip a) = pr1 a := rfl
+
+theorem flip_flip {A B : Type} (a : A × B) : flip (flip a) = a :=
+pair_destruct a (take x y, rfl)
+
+theorem P_flip {A B : Type} {P : A → B → Prop} {a : A × B} (H : P (pr1 a) (pr2 a))
+  : P (pr2 (flip a)) (pr1 (flip a)) :=
+(symm (flip_pr1 a)) ▸ (symm (flip_pr2 a)) ▸ H
+
+theorem flip_inj {A B : Type} {a b : A × B} (H : flip a = flip b) : a = b :=
+have H2 : flip (flip a) = flip (flip b), from congr_arg flip H,
+show a = b, from (flip_flip a) ▸ (flip_flip b) ▸ H2
+
+-- ### coordinatewise unary maps
+
+definition map_pair {A B : Type} (f : A → B) (a : A × A) : B × B :=
+pair (f (pr1 a)) (f (pr2 a))
+
+theorem map_pair_def {A B : Type} (f : A → B) (a : A × A)
+  : map_pair f a = pair (f (pr1 a)) (f (pr2 a)) :=
+rfl
+
+theorem map_pair_pair {A B : Type} (f : A → B) (a a' : A)
+  : map_pair f (pair a a') = pair (f a) (f a') :=
+(pr1_pair a a') ▸ (pr2_pair a a') ▸ (rfl)
+
+theorem map_pair_pr1 {A B : Type} (f : A → B) (a : A × A) : pr1 (map_pair f a) = f (pr1 a) :=
+pr1_pair _ _
+
+theorem map_pair_pr2 {A B : Type} (f : A → B) (a : A × A) : pr2 (map_pair f a) = f (pr2 a) :=
+pr2_pair _ _
+
+-- ### coordinatewise binary maps
+
+definition map_pair2 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) : C × C :=
+pair (f (pr1 a) (pr1 b)) (f (pr2 a) (pr2 b))
+
+theorem map_pair2_def {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
+  map_pair2 f a b = pair (f (pr1 a) (pr1 b)) (f (pr2 a) (pr2 b)) := rfl
+
+theorem map_pair2_pair {A B C : Type} (f : A → B → C) (a a' : A) (b b' : B) :
+  map_pair2 f (pair a a') (pair b b') = pair (f a b) (f a' b') :=
+calc
+  map_pair2 f (pair a a') (pair b b')
+        = pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) (pr2 (pair b b')))
+            : {pr1_pair b b'}
+    ... = pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) b') : {pr2_pair b b'}
+    ... = pair (f (pr1 (pair a a')) b) (f a' b') : {pr2_pair a a'}
+    ... = pair (f a b) (f a' b') : {pr1_pair a a'}
+
+theorem map_pair2_pr1 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
+pr1 (map_pair2 f a b) = f (pr1 a) (pr1 b) := pr1_pair _ _
+
+theorem map_pair2_pr2 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
+pr2 (map_pair2 f a b) = f (pr2 a) (pr2 b) := pr2_pair _ _
+
+theorem map_pair2_flip {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
+  flip (map_pair2 f a b) = map_pair2 f (flip a) (flip b) :=
+have Hx : pr1 (flip (map_pair2 f a b)) =  pr1 (map_pair2 f (flip a) (flip b)), from
+  calc
+    pr1 (flip (map_pair2 f a b)) = pr2 (map_pair2 f a b) : flip_pr1 _
+      ... = f (pr2 a) (pr2 b) : map_pair2_pr2 f a b
+      ... = f (pr1 (flip a)) (pr2 b) : {symm (flip_pr1 a)}
+      ... = f (pr1 (flip a)) (pr1 (flip b)) : {symm (flip_pr1 b)}
+      ... = pr1 (map_pair2 f (flip a) (flip b)) : symm (map_pair2_pr1 f _ _),
+have Hy : pr2 (flip (map_pair2 f a b)) =  pr2 (map_pair2 f (flip a) (flip b)), from
+  calc
+    pr2 (flip (map_pair2 f a b)) = pr1 (map_pair2 f a b) : flip_pr2 _
+      ... = f (pr1 a) (pr1 b) : map_pair2_pr1 f a b
+      ... = f (pr2 (flip a)) (pr1 b) : {symm (flip_pr2 a)}
+      ... = f (pr2 (flip a)) (pr2 (flip b)) : {symm (flip_pr2 b)}
+      ... = pr2 (map_pair2 f (flip a) (flip b)) : symm (map_pair2_pr2 f _ _),
+pair_eq Hx Hy
+
+-- add_rewrite flip_pr1 flip_pr2 flip_pair
+-- add_rewrite map_pair_pr1 map_pair_pr2 map_pair_pair
+-- add_rewrite map_pair2_pr1 map_pair2_pr2 map_pair2_pair
+
+theorem map_pair2_comm {A B : Type} {f : A → A → B} (Hcomm : ∀a b : A, f a b = f b a)
+  (v w : A × A) : map_pair2 f v w = map_pair2 f w v :=
+have Hx : pr1 (map_pair2 f v w) = pr1 (map_pair2 f w v), from
+  calc
+    pr1 (map_pair2 f v w) = f (pr1 v) (pr1 w) : map_pair2_pr1 f v w
+      ... = f (pr1 w) (pr1 v) : Hcomm _ _
+      ... = pr1 (map_pair2 f w v) : symm (map_pair2_pr1 f w v),
+have Hy : pr2 (map_pair2 f v w) = pr2 (map_pair2 f w v), from
+  calc
+    pr2 (map_pair2 f v w) = f (pr2 v) (pr2 w) : map_pair2_pr2 f v w
+      ... = f (pr2 w) (pr2 v) : Hcomm _ _
+      ... = pr2 (map_pair2 f w v) : symm (map_pair2_pr2 f w v),
+pair_eq Hx Hy
+
+theorem map_pair2_assoc {A : Type} {f : A → A → A}
+    (Hassoc : ∀a b c : A, f (f a b) c = f a (f b c)) (u v w : A × A) :
+  map_pair2 f (map_pair2 f u v) w = map_pair2 f u (map_pair2 f v w) :=
+have Hx : pr1 (map_pair2 f (map_pair2 f u v) w) =
+          pr1 (map_pair2 f u (map_pair2 f v w)), from
+  calc
+     pr1 (map_pair2 f (map_pair2 f u v) w)
+          = f (pr1 (map_pair2 f u v)) (pr1 w) : map_pair2_pr1 f _ _
+      ... = f (f (pr1 u) (pr1 v)) (pr1 w) : {map_pair2_pr1 f _ _}
+      ... = f (pr1 u) (f (pr1 v) (pr1 w)) : Hassoc (pr1 u) (pr1 v) (pr1 w)
+      ... = f (pr1 u) (pr1 (map_pair2 f v w)) : {symm (map_pair2_pr1 f _ _)}
+      ... = pr1 (map_pair2 f u (map_pair2 f v w)) : symm (map_pair2_pr1 f _ _),
+have Hy : pr2 (map_pair2 f (map_pair2 f u v) w) =
+          pr2 (map_pair2 f u (map_pair2 f v w)), from
+  calc
+     pr2 (map_pair2 f (map_pair2 f u v) w)
+          = f (pr2 (map_pair2 f u v)) (pr2 w) : map_pair2_pr2 f _ _
+      ... = f (f (pr2 u) (pr2 v)) (pr2 w) : {map_pair2_pr2 f _ _}
+      ... = f (pr2 u) (f (pr2 v) (pr2 w)) : Hassoc (pr2 u) (pr2 v) (pr2 w)
+      ... = f (pr2 u) (pr2 (map_pair2 f v w)) : {symm (map_pair2_pr2 f _ _)}
+      ... = pr2 (map_pair2 f u (map_pair2 f v w)) : symm (map_pair2_pr2 f _ _),
+pair_eq Hx Hy
+
+theorem map_pair2_id_right {A B : Type} {f : A → B → A} {e : B} (Hid : ∀a : A, f a e = a)
+  (v : A × A) : map_pair2 f v (pair e e) = v :=
+have Hx : pr1 (map_pair2 f v (pair e e)) = pr1 v, from
+  (calc
+    pr1 (map_pair2 f v (pair e e)) = f (pr1 v) (pr1 (pair e e)) : by simp
+      ... = f (pr1 v) e : by simp
+      ... = pr1 v : Hid (pr1 v)),
+have Hy : pr2 (map_pair2 f v (pair e e)) = pr2 v, from
+  (calc
+    pr2 (map_pair2 f v (pair e e)) = f (pr2 v) (pr2 (pair e e)) : by simp
+      ... = f (pr2 v) e : by simp
+      ... = pr2 v : Hid (pr2 v)),
+prod_eq Hx Hy
+
+theorem map_pair2_id_left {A B : Type} {f : B → A → A} {e : B} (Hid : ∀a : A, f e a = a)
+  (v : A × A) : map_pair2 f (pair e e) v = v :=
+have Hx : pr1 (map_pair2 f (pair e e) v) = pr1 v, from
+   calc
+    pr1 (map_pair2 f (pair e e) v) = f (pr1 (pair e e)) (pr1 v) : by simp
+      ... = f e (pr1 v) : by simp
+      ... = pr1 v : Hid (pr1 v),
+have Hy : pr2 (map_pair2 f (pair e e) v) = pr2 v, from
+   calc
+    pr2 (map_pair2 f (pair e e) v) = f (pr2 (pair e e)) (pr2 v) : by simp
+      ... = f e (pr2 v) : by simp
+      ... = pr2 v : Hid (pr2 v),
+prod_eq Hx Hy
+
+opaque_hint (hiding flip map_pair map_pair2)
+
+end quotient
diff --git a/library/standard/data/quotient.lean b/library/standard/data/quotient/basic.lean
similarity index 54%
rename from library/standard/data/quotient.lean
rename to library/standard/data/quotient/basic.lean
index 02e9248f6..eaaaf7164 100644
--- a/library/standard/data/quotient.lean
+++ b/library/standard/data/quotient/basic.lean
@@ -2,197 +2,11 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Floris van Doorn
 
-import logic tools.tactic .subtype logic.connectives.cast struc.relation data.prod
+import logic tools.tactic ..subtype logic.connectives.cast struc.relation data.prod
 import logic.connectives.instances
+import .aux
 
--- for now: to use substitution (iff_to_eq)
-import logic.axioms.classical
-
--- for the last section
-import logic.axioms.hilbert logic.axioms.funext
-
-using relation prod tactic eq_proofs
-
-
--- temporary: substiution for iff
-theorem substi {a b : Prop} {P : Prop → Prop} (H1 : a ↔ b) (H2 : P a) : P b :=
-subst (iff_to_eq H1) H2
-
-theorem transi {a b c : Prop} (H1 : a ↔ b) (H2 : b ↔ c) : a ↔ c :=
-eq_to_iff (trans (iff_to_eq H1) (iff_to_eq H2))
-
-theorem symmi {a b : Prop} (H : a ↔ b) : b ↔ a :=
-eq_to_iff (symm (iff_to_eq H))
-
--- until we have the simplifier...
-definition simp : tactic := apply @sorry
-
-
--- TODO: find a better name, and move to logic.connectives.basic
-theorem and_inhabited_left {a : Prop} (b : Prop) (Ha : a) : a ∧ b ↔ b :=
-iff_intro (take Hab, and_elim_right Hab) (take Hb, and_intro Ha Hb)
-
-
--- auxliary facts about products
--- -----------------------------
-
--- TODO: move to data.prod?
-
--- ### flip
-
-definition flip {A B : Type} (a : A × B) : B × A := pair (pr2 a) (pr1 a)
-
-theorem flip_def {A B : Type} (a : A × B) : flip a = pair (pr2 a) (pr1 a) := refl (flip a)
-
-theorem flip_pair {A B : Type} (a : A) (b : B) : flip (pair a b) = pair b a := rfl
-
-theorem flip_pr1 {A B : Type} (a : A × B) : pr1 (flip a) = pr2 a := rfl
-
-theorem flip_pr2 {A B : Type} (a : A × B) : pr2 (flip a) = pr1 a := rfl
-
-theorem flip_flip {A B : Type} (a : A × B) : flip (flip a) = a := 
-pair_destruct a (take x y, rfl)
-
-theorem P_flip {A B : Type} {P : A → B → Prop} {a : A × B} (H : P (pr1 a) (pr2 a))
-  : P (pr2 (flip a)) (pr1 (flip a)) :=
-(symm (flip_pr1 a)) ▸ (symm (flip_pr2 a)) ▸ H
-
-theorem flip_inj {A B : Type} {a b : A × B} (H : flip a = flip b) : a = b :=
-have H2 : flip (flip a) = flip (flip b), from congr2 flip H,
-show a = b, from (flip_flip a) ▸ (flip_flip b) ▸ H2
-
--- ### coordinatewise unary maps
-
-definition map_pair {A B : Type} (f : A → B) (a : A × A) : B × B := 
-pair (f (pr1 a)) (f (pr2 a))
-
-theorem map_pair_def {A B : Type} (f : A → B) (a : A × A)
-  : map_pair f a = pair (f (pr1 a)) (f (pr2 a)) := 
-rfl
-
-theorem map_pair_pair {A B : Type} (f : A → B) (a a' : A)
-  : map_pair f (pair a a') = pair (f a) (f a') := 
-(pr1_pair a a') ▸ (pr2_pair a a') ▸ (rfl)
-
-theorem map_pair_pr1 {A B : Type} (f : A → B) (a : A × A) : pr1 (map_pair f a) = f (pr1 a)
-:= pr1_pair _ _
-
-theorem map_pair_pr2 {A B : Type} (f : A → B) (a : A × A) : pr2 (map_pair f a) = f (pr2 a)
-:= pr2_pair _ _
-
--- ### coordinatewise binary maps
-
-definition map_pair2 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) : C × C
-:= pair (f (pr1 a) (pr1 b)) (f (pr2 a) (pr2 b))
-
-theorem map_pair2_def {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B)
-  : map_pair2 f a b = pair (f (pr1 a) (pr1 b)) (f (pr2 a) (pr2 b)) := rfl
-
-theorem map_pair2_pair {A B C : Type} (f : A → B → C) (a a' : A) (b b' : B)
-  : map_pair2 f (pair a a') (pair b b') = pair (f a b) (f a' b') :=
-calc
-  map_pair2 f (pair a a') (pair b b')
-	= pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) (pr2 (pair b b')))
-	    : {pr1_pair b b'}
-    ... = pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) b') : {pr2_pair b b'}
-    ... = pair (f (pr1 (pair a a')) b) (f a' b') : {pr2_pair a a'}
-    ... = pair (f a b) (f a' b') : {pr1_pair a a'}
-
-theorem map_pair2_pr1 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B)
-  : pr1 (map_pair2 f a b) = f (pr1 a) (pr1 b) := pr1_pair _ _
-
-theorem map_pair2_pr2 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B)
-  : pr2 (map_pair2 f a b) = f (pr2 a) (pr2 b) := pr2_pair _ _
-
-theorem map_pair2_flip {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B)
-  : flip (map_pair2 f a b) = map_pair2 f (flip a) (flip b) :=
-  have Hx : pr1 (flip (map_pair2 f a b)) =  pr1 (map_pair2 f (flip a) (flip b)), from
-    calc
-      pr1 (flip (map_pair2 f a b)) = pr2 (map_pair2 f a b) : flip_pr1 _
-        ... = f (pr2 a) (pr2 b) : map_pair2_pr2 f a b
-        ... = f (pr1 (flip a)) (pr2 b) : {symm (flip_pr1 a)}
-        ... = f (pr1 (flip a)) (pr1 (flip b)) : {symm (flip_pr1 b)}
-        ... = pr1 (map_pair2 f (flip a) (flip b)) : symm (map_pair2_pr1 f _ _),
-  have Hy : pr2 (flip (map_pair2 f a b)) =  pr2 (map_pair2 f (flip a) (flip b)), from
-    calc
-      pr2 (flip (map_pair2 f a b)) = pr1 (map_pair2 f a b) : flip_pr2 _
-        ... = f (pr1 a) (pr1 b) : map_pair2_pr1 f a b
-        ... = f (pr2 (flip a)) (pr1 b) : {symm (flip_pr2 a)}
-        ... = f (pr2 (flip a)) (pr2 (flip b)) : {symm (flip_pr2 b)}
-        ... = pr2 (map_pair2 f (flip a) (flip b)) : symm (map_pair2_pr2 f _ _),
-  pair_eq Hx Hy
-
--- add_rewrite flip_pr1 flip_pr2 flip_pair
--- add_rewrite map_pair_pr1 map_pair_pr2 map_pair_pair
--- add_rewrite map_pair2_pr1 map_pair2_pr2 map_pair2_pair
-
-theorem map_pair2_comm {A B : Type} {f : A → A → B} (Hcomm : ∀a b : A, f a b = f b a)
-  (v w : A × A) : map_pair2 f v w = map_pair2 f w v :=
-have Hx : pr1 (map_pair2 f v w) = pr1 (map_pair2 f w v), from
-  calc
-    pr1 (map_pair2 f v w) = f (pr1 v) (pr1 w) : map_pair2_pr1 f v w
-      ... = f (pr1 w) (pr1 v) : Hcomm _ _
-      ... = pr1 (map_pair2 f w v) : symm (map_pair2_pr1 f w v),
-have Hy : pr2 (map_pair2 f v w) = pr2 (map_pair2 f w v), from
-  calc
-    pr2 (map_pair2 f v w) = f (pr2 v) (pr2 w) : map_pair2_pr2 f v w
-      ... = f (pr2 w) (pr2 v) : Hcomm _ _
-      ... = pr2 (map_pair2 f w v) : symm (map_pair2_pr2 f w v),
-pair_eq Hx Hy
-
-theorem map_pair2_assoc {A : Type} {f : A → A → A}
-    (Hassoc : ∀a b c : A, f (f a b) c = f a (f b c)) (u v w : A × A) : 
-  map_pair2 f (map_pair2 f u v) w = map_pair2 f u (map_pair2 f v w) :=
-have Hx : pr1 (map_pair2 f (map_pair2 f u v) w) =
-	  pr1 (map_pair2 f u (map_pair2 f v w)), from
-  calc
-     pr1 (map_pair2 f (map_pair2 f u v) w)
-	  = f (pr1 (map_pair2 f u v)) (pr1 w) : map_pair2_pr1 f _ _
-      ... = f (f (pr1 u) (pr1 v)) (pr1 w) : {map_pair2_pr1 f _ _}
-      ... = f (pr1 u) (f (pr1 v) (pr1 w)) : Hassoc (pr1 u) (pr1 v) (pr1 w)
-      ... = f (pr1 u) (pr1 (map_pair2 f v w)) : {symm (map_pair2_pr1 f _ _)}
-      ... = pr1 (map_pair2 f u (map_pair2 f v w)) : symm (map_pair2_pr1 f _ _),
-have Hy : pr2 (map_pair2 f (map_pair2 f u v) w) =
-	  pr2 (map_pair2 f u (map_pair2 f v w)), from
-  calc
-     pr2 (map_pair2 f (map_pair2 f u v) w)
-	  = f (pr2 (map_pair2 f u v)) (pr2 w) : map_pair2_pr2 f _ _
-      ... = f (f (pr2 u) (pr2 v)) (pr2 w) : {map_pair2_pr2 f _ _}
-      ... = f (pr2 u) (f (pr2 v) (pr2 w)) : Hassoc (pr2 u) (pr2 v) (pr2 w)
-      ... = f (pr2 u) (pr2 (map_pair2 f v w)) : {symm (map_pair2_pr2 f _ _)}
-      ... = pr2 (map_pair2 f u (map_pair2 f v w)) : symm (map_pair2_pr2 f _ _),
-pair_eq Hx Hy
-
-theorem map_pair2_id_right {A B : Type} {f : A → B → A} {e : B} (Hid : ∀a : A, f a e = a) 
-  (v : A × A) : map_pair2 f v (pair e e) = v :=
-have Hx : pr1 (map_pair2 f v (pair e e)) = pr1 v, from
-  (calc
-    pr1 (map_pair2 f v (pair e e)) = f (pr1 v) (pr1 (pair e e)) : by simp
-      ... = f (pr1 v) e : by simp
-      ... = pr1 v : Hid (pr1 v)),
-have Hy : pr2 (map_pair2 f v (pair e e)) = pr2 v, from
-  (calc
-    pr2 (map_pair2 f v (pair e e)) = f (pr2 v) (pr2 (pair e e)) : by simp
-      ... = f (pr2 v) e : by simp
-      ... = pr2 v : Hid (pr2 v)),
-prod_eq Hx Hy
-
-theorem map_pair2_id_left {A B : Type} {f : B → A → A} {e : B} (Hid : ∀a : A, f e a = a)
-  (v : A × A) : map_pair2 f (pair e e) v = v :=
-have Hx : pr1 (map_pair2 f (pair e e) v) = pr1 v, from
-   calc
-    pr1 (map_pair2 f (pair e e) v) = f (pr1 (pair e e)) (pr1 v) : by simp
-      ... = f e (pr1 v) : by simp
-      ... = pr1 v : Hid (pr1 v),
-have Hy : pr2 (map_pair2 f (pair e e) v) = pr2 v, from
-   calc
-    pr2 (map_pair2 f (pair e e) v) = f (pr2 (pair e e)) (pr2 v) : by simp
-      ... = f e (pr2 v) : by simp
-      ... = pr2 v : Hid (pr2 v),
-prod_eq Hx Hy
-
-opaque_hint (hiding flip map_pair map_pair2)
-
+using relation prod inhabited nonempty tactic eq_ops
 
 -- Theory data.quotient
 -- ====================
@@ -205,7 +19,7 @@ using subtype
 -- ---------------------
 
 -- TODO: make this a structure
-definition is_quotient {A B : Type} (R : A → A → Prop) (abs : A → B) (rep : B → A) : Prop :=
+abbreviation is_quotient {A B : Type} (R : A → A → Prop) (abs : A → B) (rep : B → A) : Prop :=
   (∀b, abs (rep b) = b) ∧
   (∀b, R (rep b) (rep b)) ∧
   (∀r s, R r s ↔ (R r r ∧ R s s ∧ abs r = abs s))
@@ -224,8 +38,8 @@ and_intro H1 (and_intro H2 H3)
 --   (take r s,
 --     have H4 : R r s ↔ R s s ∧ abs r = abs s,
 --       from 
---         gensubst.subst (relation.operations.symm (and_inhabited_left _ (H1 s))) (H3 r s),
---     gensubst.subst (relation.operations.symm (and_inhabited_left _ (H1 r))) H4)
+--         gensubst.subst (relation.operations.symm (and_absorb_left _ (H1 s))) (H3 r s),
+--     gensubst.subst (relation.operations.symm (and_absorb_left _ (H1 r))) H4)
 
 -- these work now, but the above still does not
 -- theorem test (a b c : Prop) (P : Prop → Prop) (H1 : a ↔ b) (H2 : c ∧ a) : c ∧ b :=
@@ -233,7 +47,7 @@ and_intro H1 (and_intro H2 H3)
 
 -- theorem test2 {A : Type} {R : A → A → Prop} (Q : Prop) (r s : A) 
 --   (H3 : R r s ↔ Q) (H1 : R s s) : Q ↔ (R s s ∧ Q) :=
--- relation.operations.symm (and_inhabited_left Q H1)
+-- relation.operations.symm (and_absorb_left Q H1)
 
 -- theorem test3 {A : Type} {R : A → A → Prop} (Q : Prop) (r s : A) 
 --   (H3 : R r s ↔ Q) (H1 : R s s) : R r s ↔ (R s s ∧ Q) :=
@@ -241,7 +55,10 @@ and_intro H1 (and_intro H2 H3)
 
 -- theorem test4 {A : Type} {R : A → A → Prop} (Q : Prop) (r s : A) 
 --   (H3 : R r s ↔ Q) (H1 : R s s) : R r s ↔ (R s s ∧ Q) :=
--- gensubst.subst (relation.operations.symm (and_inhabited_left Q H1)) H3
+-- gensubst.subst (relation.operations.symm (and_absorb_left Q H1)) H3
+
+theorem and_absorb_left {a : Prop} (b : Prop) (Ha : a) : a ∧ b ↔ b :=
+iff_intro (assume Hab, and_elim_right Hab) (assume Hb, and_intro Ha Hb)
 
 theorem intro_refl {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
   (H1 : reflexive R) (H2 : ∀b, abs (rep b) = b)
@@ -252,8 +69,20 @@ intro
   (take r s,
     have H4 : R r s ↔ R s s ∧ abs r = abs s,
       from 
-        substi (symmi (and_inhabited_left _ (H1 s))) (H3 r s),
-    substi (symmi (and_inhabited_left _ (H1 r))) H4)
+        subst_iff (iff_symm (and_absorb_left _ (H1 s))) (H3 r s),
+    subst_iff (iff_symm (and_absorb_left _ (H1 r))) H4)
+
+-- theorem intro_refl {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
+--   (H1 : reflexive R) (H2 : ∀b, abs (rep b) = b)
+--   (H3 : ∀r s, R r s ↔ abs r = abs s) : is_quotient R abs rep :=
+-- intro
+--   H2
+--   (take b, H1 (rep b))
+--   (take r s,
+--     have H4 : R r s ↔ R s s ∧ abs r = abs s,
+--       from 
+--         substi (iff_symm (and_absorb_left _ (H1 s))) (H3 r s),
+--     substi (iff_symm (and_absorb_left _ (H1 r))) H4)
 
 theorem abs_rep {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
   (Q : is_quotient R abs rep) (b : B) :  abs (rep b) = b := 
@@ -414,10 +243,10 @@ opaque_hint (hiding rec rec_constant rec_binary quotient_map quotient_map_binary
 abbreviation image {A B : Type} (f : A → B) := subtype (fun b, ∃a, f a = b)
 
 theorem image_inhabited {A B : Type} (f : A → B) (H : inhabited A) : inhabited (image f) :=
-inhabited_intro (tag (f (default A)) (exists_intro (default A) rfl))
+inhabited_mk (tag (f (default A)) (exists_intro (default A) rfl))
 
 theorem image_inhabited2 {A B : Type} (f : A → B) (a : A) : inhabited (image f) :=
-image_inhabited f (inhabited_intro a)
+image_inhabited f (inhabited_mk a)
 
 definition fun_image {A B : Type} (f : A → B) (a : A) : image f :=
 tag (f a) (exists_intro a rfl)
@@ -446,7 +275,7 @@ theorem fun_image_eq {A B : Type} (f : A → B) (a a' : A)
 iff_intro
   (assume H : f a = f a', tag_eq H)
   (assume H : fun_image f a = fun_image f a',
-    subst (subst (congr2 elt_of H) (elt_of_fun_image f a)) (elt_of_fun_image f a'))
+    subst (subst (congr_arg elt_of H) (elt_of_fun_image f a)) (elt_of_fun_image f a'))
 
 theorem idempotent_image_elt_of {A : Type} {f : A → A} (H : ∀a, f (f a) = f a) (u : image f)
   : fun_image f (elt_of u) = u :=
@@ -508,89 +337,30 @@ intro
       obtain (a : A) (Ha : f a = elt_of u), from image_elt_of u,
         subst Ha (@representative_map_refl_rep A R f H1 H2 a))
   (take a a', 
-    substi (fun_image_eq f a a') (H2 a a'))
-
--- TODO: fix these
--- e.g. in the next three lemmas, we should not need to specify the equivalence relation
--- but the class inference finds reflexive.class eq
-theorem equiv_is_refl {A : Type} {R : A → A → Prop} (equiv : is_equivalence.class R) :=
-@operations.refl _ R (@is_equivalence.is_reflexive _ _ equiv)
--- we should be able to write
--- @operations.refl _ R _
-
-theorem equiv_is_symm {A : Type} {R : A → A → Prop} (equiv : is_equivalence.class R) :=
-@operations.symm _ R (@is_equivalence.is_symmetric _ _ equiv)
-
-theorem equiv_is_trans {A : Type} {R : A → A → Prop} (equiv : is_equivalence.class R) :=
-@operations.trans _ R (@is_equivalence.is_transitive _ _ equiv)
+    subst_iff (fun_image_eq f a a') (H2 a a'))
 
 theorem representative_map_equiv_inj {A : Type} {R : A → A → Prop}
-  (equiv : is_equivalence.class R) {f : A → A} (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b → f a = f b)
+  (equiv : is_equivalence R) {f : A → A} (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b → f a = f b)
   {a b : A} (H3 : f a = f b) : R a b :=
--- have symmR : symmetric R, from @relation.operations.symm _ R _,
-have symmR : symmetric R, from equiv_is_symm equiv,
-have transR : transitive R, from equiv_is_trans equiv,
+have symmR : symmetric R, from is_symmetric.infer R,
+have transR : transitive R, from is_transitive.infer R,
 show R a b, from
   have H2 : R a (f b), from subst H3 (H1 a),
-  have H3 : R (f b) b, from symmR _ _ (H1 b),
-  transR _ _ _ H2 H3
+  have H3 : R (f b) b, from symmR (H1 b),
+  transR H2 H3
 
 theorem representative_map_to_quotient_equiv {A : Type} {R : A → A → Prop}
-  (equiv : is_equivalence.class R) {f : A → A} (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b → f a = f b)
+  (equiv : is_equivalence R) {f : A → A} (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b → f a = f b)
   : @is_quotient A (image f) R (fun_image f) elt_of :=
 representative_map_to_quotient
   H1
   (take a b,
-    have reflR : reflexive R, from equiv_is_refl equiv,
+    have reflR : reflexive R, from is_reflexive.infer R,
     have H3 : f a = f b → R a b, from representative_map_equiv_inj equiv H1 H2,
     have H4 : R a b ↔ f a = f b, from iff_intro (H2 a b) H3,
     have H5 : R a b ↔ R b b ∧ f a = f b,
-      from substi (symmi (and_inhabited_left _ (reflR b))) H4,
-    substi (symmi (and_inhabited_left _ (reflR a))) H5)
-
--- TODO: split this into another file -- it depends on hilbert
-
--- abstract quotient
--- -----------------
-
-definition prelim_map {A : Type} (R : A → A → Prop) (a : A) :=
--- TODO: it is interesting how the elaborator fails here
--- epsilon (fun b, R a b)
-@epsilon _ (nonempty_intro a) (fun b, R a b)
-
--- TODO: only needed R reflexive (or weaker: R a a)
-theorem prelim_map_rel {A : Type} {R : A → A → Prop} (H : is_equivalence.class R) (a : A)
-  : R a (prelim_map R a) :=
-have reflR : reflexive R, from equiv_is_refl H,
-epsilon_spec (exists_intro a (reflR a))
-
--- TODO: only needed: R PER
-theorem prelim_map_congr {A : Type} {R : A → A → Prop} (H1 : is_equivalence.class R) {a b : A}
-  (H2 : R a b) : prelim_map R a = prelim_map R b :=
-have symmR : symmetric R, from equiv_is_symm H1,
-have transR : transitive R, from equiv_is_trans H1,
-have H3 : ∀c, R a c ↔ R b c, from
-  take c,
-    iff_intro
-      (assume H4 : R a c, transR b a c (symmR a b H2) H4)
-      (assume H4 : R b c, transR a b c H2 H4),
-have H4 : (fun c, R a c) = (fun c, R b c), from funext (take c, iff_to_eq (H3 c)),
-show @epsilon _ (nonempty_intro a) (λc, R a c) = @epsilon _ (nonempty_intro b) (λc, R b c), 
-  from congr2 _ H4
-
-definition quotient {A : Type} (R : A → A → Prop) : Type := image (prelim_map R)
-
-definition quotient_abs {A : Type} (R : A → A → Prop) : A → quotient R :=
-fun_image (prelim_map R)
-
-definition quotient_elt_of {A : Type} (R : A → A → Prop) : quotient R → A := elt_of
-
-theorem quotient_is_quotient  {A : Type} (R : A → A → Prop) (H : is_equivalence.class R)
-  : is_quotient R (quotient_abs R) (quotient_elt_of R) :=
-representative_map_to_quotient_equiv
-  H
-  (prelim_map_rel H)
-  (@prelim_map_congr _ _ H)
+      from subst_iff (iff_symm (and_absorb_left _ (reflR b))) H4,
+    subst_iff (iff_symm (and_absorb_left _ (reflR a))) H5)
 
 -- previously:
 -- opaque_hint (hiding fun_image rec is_quotient prelim_map)
diff --git a/library/standard/data/quotient/classical.lean b/library/standard/data/quotient/classical.lean
new file mode 100644
index 000000000..ba234cb7a
--- /dev/null
+++ b/library/standard/data/quotient/classical.lean
@@ -0,0 +1,56 @@
+-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Floris van Doorn
+
+import struc.relation logic.classes.nonempty data.subtype
+import .basic
+import logic.axioms.classical logic.axioms.hilbert logic.axioms.funext
+
+namespace quotient
+
+using relation nonempty subtype
+
+-- abstract quotient
+-- -----------------
+
+definition prelim_map {A : Type} (R : A → A → Prop) (a : A) :=
+-- TODO: it is interesting how the elaborator fails here
+-- epsilon (fun b, R a b)
+@epsilon _ (nonempty_intro a) (fun b, R a b)
+
+-- TODO: only needed R reflexive (or weaker: R a a)
+theorem prelim_map_rel {A : Type} {R : A → A → Prop} (H : is_equivalence R) (a : A)
+  : R a (prelim_map R a) :=
+have reflR : reflexive R, from is_reflexive.infer R,
+epsilon_spec (exists_intro a (reflR a))
+
+-- TODO: only needed: R PER
+theorem prelim_map_congr {A : Type} {R : A → A → Prop} (H1 : is_equivalence R) {a b : A}
+  (H2 : R a b) : prelim_map R a = prelim_map R b :=
+have symmR : symmetric R, from is_symmetric.infer R,
+have transR : transitive R, from is_transitive.infer R,
+have H3 : ∀c, R a c ↔ R b c, from
+  take c,
+    iff_intro
+      (assume H4 : R a c, transR (symmR H2) H4)
+      (assume H4 : R b c, transR H2 H4),
+have H4 : (fun c, R a c) = (fun c, R b c), from funext (take c, iff_to_eq (H3 c)),
+show @epsilon _ (nonempty_intro a) (λc, R a c) = @epsilon _ (nonempty_intro b) (λc, R b c),
+  from congr_arg _ H4
+
+definition quotient {A : Type} (R : A → A → Prop) : Type := image (prelim_map R)
+
+definition quotient_abs {A : Type} (R : A → A → Prop) : A → quotient R :=
+fun_image (prelim_map R)
+
+definition quotient_elt_of {A : Type} (R : A → A → Prop) : quotient R → A := elt_of
+
+-- TODO: I had to make is_quotient transparent -- change this?
+theorem quotient_is_quotient  {A : Type} (R : A → A → Prop) (H : is_equivalence R)
+  : is_quotient R (quotient_abs R) (quotient_elt_of R) :=
+representative_map_to_quotient_equiv
+  H
+  (prelim_map_rel H)
+  (@prelim_map_congr _ _ H)
+
+end quotient
diff --git a/library/standard/data/quotient/default.lean b/library/standard/data/quotient/default.lean
new file mode 100644
index 000000000..22d38eec9
--- /dev/null
+++ b/library/standard/data/quotient/default.lean
@@ -0,0 +1,5 @@
+--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+--- Released under Apache 2.0 license as described in the file LICENSE.
+--- Author: Jeremy Avigad
+
+import .basic .classical
diff --git a/library/standard/data/quotient/quotient.md b/library/standard/data/quotient/quotient.md
new file mode 100644
index 000000000..09bb1f145
--- /dev/null
+++ b/library/standard/data/quotient/quotient.md
@@ -0,0 +1,6 @@
+data.quotient
+=============
+
+* [aux](aux.lean) : auxiliary facts about products
+* [basic](basic.lean) : the constructive core of the quotient construction
+* [classical](classical.lean) : the classical version, using Hilbert choice
diff --git a/library/standard/data/set.lean b/library/standard/data/set.lean
index 2becfd638..382abfacf 100644
--- a/library/standard/data/set.lean
+++ b/library/standard/data/set.lean
@@ -5,7 +5,7 @@
 ----------------------------------------------------------------------------------------------------
 
 import logic.axioms.funext data.bool
-using eq_proofs bool
+using eq_ops bool
 
 namespace set
 definition set (T : Type) := T → bool
diff --git a/library/standard/data/sigma.lean b/library/standard/data/sigma.lean
index e0d9c4b95..6ef6584a2 100644
--- a/library/standard/data/sigma.lean
+++ b/library/standard/data/sigma.lean
@@ -4,6 +4,8 @@
 
 import logic.classes.inhabited logic.connectives.eq
 
+using inhabited
+
 inductive sigma {A : Type} (B : A → Type) : Type :=
 | dpair : Πx : A, B x → sigma B
 
@@ -48,7 +50,7 @@ section
 
   theorem sigma_inhabited (H1 : inhabited A) (H2 : inhabited (B (default A))) :
     inhabited (sigma B) :=
-   inhabited_elim H1 (λa, inhabited_elim H2 (λb, inhabited_intro (dpair (default A) b)))
+   inhabited_destruct H1 (λa, inhabited_destruct H2 (λb, inhabited_mk (dpair (default A) b)))
 
 end
 
diff --git a/library/standard/data/string.lean b/library/standard/data/string.lean
index 06a6cd14f..a2f5b9a64 100644
--- a/library/standard/data/string.lean
+++ b/library/standard/data/string.lean
@@ -1,13 +1,13 @@
-----------------------------------------------------------------------------------------------------
 -- 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.bool
-using bool
+
+using bool inhabited
 
 namespace string
+
 inductive char : Type :=
 | ascii : bool → bool → bool → bool → bool → bool → bool → bool → char
 
@@ -16,9 +16,9 @@ inductive string : Type :=
 | str   : char → string → string
 
 theorem inhabited_char [instance] : inhabited char :=
-inhabited_intro (ascii ff ff ff ff ff ff ff ff)
+inhabited_mk (ascii ff ff ff ff ff ff ff ff)
 
 theorem inhabited_string [instance] : inhabited string :=
-inhabited_intro empty
+inhabited_mk empty
 
 end string
diff --git a/library/standard/data/unit.lean b/library/standard/data/unit.lean
index cac908449..a6c7eb88b 100644
--- a/library/standard/data/unit.lean
+++ b/library/standard/data/unit.lean
@@ -17,8 +17,8 @@ theorem unit_eq (a b : unit) : a = b :=
 unit_rec (unit_rec (refl ⋆) b) a
 
 theorem inhabited_unit [instance] : inhabited unit :=
-inhabited_intro ⋆
+inhabited_mk ⋆
 
 theorem decidable_eq [instance] (a b : unit) : decidable (a = b) :=
 inl (unit_eq a b)
-end unit
\ No newline at end of file
+end unit
diff --git a/library/standard/hott/inhabited.lean b/library/standard/hott/inhabited.lean
deleted file mode 100644
index 0447e7a0f..000000000
--- a/library/standard/hott/inhabited.lean
+++ /dev/null
@@ -1,40 +0,0 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Leonardo de Moura
-
--- The predicative version of inhabited
--- TODO: restore instances
-
--- import logic bool
--- using logic
-
-namespace predicative
-
-inductive inhabited (A : Type) : Type :=
-| inhabited_intro : A → inhabited A
-
-theorem inhabited_elim {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B
-:= inhabited_rec H2 H1
-
-end predicative
-
--- theorem inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B)
--- := inhabited_elim H (take (b : B), inhabited_intro (λ a : A, b))
-
--- theorem inhabited_sum_left [instance] {A : Type} (B : Type) (H : inhabited A) : inhabited (A + B)
--- := inhabited_elim H (λ a, inhabited_intro (inl B a))
-
--- theorem inhabited_sum_right [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A + B)
--- := inhabited_elim H (λ b, inhabited_intro (inr A b))
-
--- theorem inhabited_product [instance] {A : Type} {B : Type} (Ha : inhabited A) (Hb : inhabited B) : inhabited (A × B)
--- := inhabited_elim Ha (λ a, (inhabited_elim Hb (λ b, inhabited_intro (a, b))))
-
--- theorem inhabited_bool [instance] : inhabited bool
--- := inhabited_intro true
-
--- theorem inhabited_unit [instance] : inhabited unit
--- := inhabited_intro ⋆
-
--- theorem inhabited_sigma_pr1 {A : Type} {B : A → Type} (p : Σ x, B x) : inhabited A
--- := inhabited_intro (dpr1 p)
diff --git a/library/standard/logic/axioms/classical.lean b/library/standard/logic/axioms/classical.lean
index 509777bf6..d5217a8ba 100644
--- a/library/standard/logic/axioms/classical.lean
+++ b/library/standard/logic/axioms/classical.lean
@@ -4,9 +4,9 @@
 -- Author: Leonardo de Moura
 ----------------------------------------------------------------------------------------------------
 
-import logic.connectives.basic logic.connectives.quantifiers logic.connectives.cast
+import logic.connectives.basic logic.connectives.quantifiers logic.connectives.cast struc.relation
 
-using eq_proofs
+using eq_ops
 
 axiom prop_complete (a : Prop) : a = true ∨ a = false
 
@@ -15,6 +15,9 @@ or_elim (prop_complete a)
   (assume Ht : a = true,  Ht⁻¹ ▸ H1)
   (assume Hf : a = false, Hf⁻¹ ▸ H2)
 
+theorem case_on (a : Prop) {P : Prop → Prop} (H1 : P true) (H2 : P false) : P a :=
+case P H1 H2 a
+
 theorem em (a : Prop) : a ∨ ¬a :=
 or_elim (prop_complete a)
   (assume Ht : a = true,  or_inl (eqt_elim Ht))
@@ -163,3 +166,12 @@ theorem peirce (a b : Prop) : ((a → b) → a) → a :=
 assume H, by_contradiction (assume Hna : ¬a,
   have Hnna : ¬¬a, from not_implies_left (mt H Hna),
   absurd (not_not_elim Hnna) Hna)
+
+-- with classical logic, every predicate respects iff
+
+using relation
+theorem iff_congr [instance] (P : Prop → Prop) : congr iff iff P :=
+congr_mk
+  (take (a b : Prop),
+    assume H : a ↔ b,
+    show P a ↔ P b, from eq_to_iff (subst (iff_to_eq H) (refl (P a))))
diff --git a/library/standard/logic/axioms/examples/diaconescu.lean b/library/standard/logic/axioms/examples/diaconescu.lean
index c0081207c..cbfae2fb0 100644
--- a/library/standard/logic/axioms/examples/diaconescu.lean
+++ b/library/standard/logic/axioms/examples/diaconescu.lean
@@ -3,7 +3,7 @@
 -- Author: Leonardo de Moura
 
 import logic.axioms.hilbert logic.axioms.funext
-using eq_proofs
+using eq_ops nonempty inhabited
 
 -- Diaconescu’s theorem
 -- Show that Excluded middle follows from
diff --git a/library/standard/logic/axioms/hilbert.lean b/library/standard/logic/axioms/hilbert.lean
index 8cc04b759..373791605 100644
--- a/library/standard/logic/axioms/hilbert.lean
+++ b/library/standard/logic/axioms/hilbert.lean
@@ -6,7 +6,7 @@ import logic.connectives.eq logic.connectives.quantifiers
 import logic.classes.inhabited logic.classes.nonempty
 import data.subtype data.sum
 
-using subtype
+using subtype inhabited nonempty
 
 -- logic.axioms.hilbert
 -- ====================
@@ -25,7 +25,7 @@ nonempty_elim H (take x, exists_intro x trivial)
 
 theorem nonempty_imp_inhabited {A : Type} (H : nonempty A) : inhabited A :=
 let u : {x : A | (∃x : A, true) → true} := strong_indefinite_description (λa, true) H in
-inhabited_intro (elt_of u)
+inhabited_mk (elt_of u)
 
 theorem inhabited_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : inhabited A :=
 nonempty_imp_inhabited (obtain w Hw, from H, nonempty_intro w)
diff --git a/library/standard/logic/axioms/piext.lean b/library/standard/logic/axioms/piext.lean
index 56c17084b..b9fb633a7 100644
--- a/library/standard/logic/axioms/piext.lean
+++ b/library/standard/logic/axioms/piext.lean
@@ -6,27 +6,29 @@
 
 import logic.classes.inhabited logic.connectives.cast
 
+using inhabited
+
 -- Pi extensionality
 axiom piext {A : Type} {B B' : A → Type} {H : inhabited (Π x, B x)} :
   (Π x, B x) = (Π x, B' x) → B = B'
 
 theorem cast_app {A : Type} {B B' : A → Type} (H : (Π x, B x) = (Π x, B' x)) (f : Π x, B x)
   (a : A) : cast H f a == f a :=
-have Hi [fact] : inhabited (Π x, B x), from inhabited_intro f,
+have Hi [fact] : inhabited (Π x, B x), from inhabited_mk f,
 have Hb : B = B', from piext H,
 cast_app' Hb f a
 
-theorem hcongr1 {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A)
+theorem hcongr_fun {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A)
   (H : f == f') : f a == f' a :=
-have Hi [fact] : inhabited (Π x, B x), from inhabited_intro f,
+have Hi [fact] : inhabited (Π x, B x), from inhabited_mk f,
 have Hb : B = B', from piext (type_eq H),
-hcongr1' a H Hb
+hcongr_fun' a H Hb
 
 theorem hcongr {A A' : Type} {B : A → Type} {B' : A' → Type}
     {f : Π x, B x} {f' : Π x, B' x} {a : A} {a' : A'}
     (Hff' : f == f') (Haa' : a == a') : f a == f' a' :=
 have H1 : ∀ (B B' : A → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' a, from
-  take B B' f f' e, hcongr1 a e,
+  take B B' f f' e, hcongr_fun a e,
 have H2 : ∀ (B : A → Type) (B' : A' → Type) (f : Π x, B x) (f' : Π x, B' x),
     f == f' → f a == f' a', from hsubst Haa' H1,
 H2 B B' f f' Hff'
diff --git a/library/standard/logic/axioms/prop_decidable.lean b/library/standard/logic/axioms/prop_decidable.lean
index 984b24463..b3c1ace4a 100644
--- a/library/standard/logic/axioms/prop_decidable.lean
+++ b/library/standard/logic/axioms/prop_decidable.lean
@@ -5,7 +5,7 @@
 ----------------------------------------------------------------------------------------------------
 
 import logic.axioms.classical logic.axioms.hilbert logic.classes.decidable
-using decidable
+using decidable inhabited nonempty
 
 -- Excluded middle + Hilbert implies every proposition is decidable
 
diff --git a/library/standard/logic/classes/decidable.lean b/library/standard/logic/classes/decidable.lean
index 622aba7c0..f77b6eabe 100644
--- a/library/standard/logic/classes/decidable.lean
+++ b/library/standard/logic/classes/decidable.lean
@@ -27,12 +27,12 @@ decidable_rec H1 H2 H
 theorem irrelevant {p : Prop} (d1 d2 : decidable p) : d1 = d2 :=
 decidable_rec
   (assume Hp1 : p, decidable_rec
-    (assume Hp2  : p,  congr2 inl (refl Hp1)) -- using proof irrelevance for Prop
+    (assume Hp2  : p,  congr_arg inl (refl Hp1)) -- using proof irrelevance for Prop
     (assume Hnp2 : ¬p, absurd_elim (inl Hp1 = inr Hnp2) Hp1 Hnp2)
     d2)
   (assume Hnp1 : ¬p, decidable_rec
     (assume Hp2  : p,  absurd_elim (inr Hnp1 = inl Hp2) Hp2 Hnp1)
-    (assume Hnp2 : ¬p, congr2 inr (refl Hnp1)) -- using proof irrelevance for Prop
+    (assume Hnp2 : ¬p, congr_arg inr (refl Hnp1)) -- using proof irrelevance for Prop
     d2)
   d1
 
@@ -87,4 +87,4 @@ rec_on Ha
 theorem decidable_eq_equiv {a b : Prop} (Ha : decidable a) (H : a = b) : decidable b :=
 decidable_iff_equiv Ha (eq_to_iff H)
 
-end decidable
\ No newline at end of file
+end decidable
diff --git a/library/standard/logic/classes/inhabited.lean b/library/standard/logic/classes/inhabited.lean
index af71779ae..37bd0bf85 100644
--- a/library/standard/logic/classes/inhabited.lean
+++ b/library/standard/logic/classes/inhabited.lean
@@ -5,15 +5,19 @@
 import logic.connectives.basic
 
 inductive inhabited (A : Type) : Type :=
-| inhabited_intro : A → inhabited A
+| inhabited_mk : A → inhabited A
 
-definition inhabited_elim {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B :=
+namespace inhabited
+
+definition inhabited_destruct {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B :=
 inhabited_rec H2 H1
 
 definition inhabited_Prop [instance] : inhabited Prop :=
-inhabited_intro true
+inhabited_mk true
 
 definition inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B) :=
-inhabited_elim H (take b, inhabited_intro (λa, b))
+inhabited_destruct H (take b, inhabited_mk (λa, b))
 
-definition default (A : Type) {H : inhabited A} : A := inhabited_elim H (take a, a)
+definition default (A : Type) {H : inhabited A} : A := inhabited_destruct H (take a, a)
+
+end inhabited
diff --git a/library/standard/logic/classes/nonempty.lean b/library/standard/logic/classes/nonempty.lean
index 11c0fd5b2..e59837442 100644
--- a/library/standard/logic/classes/nonempty.lean
+++ b/library/standard/logic/classes/nonempty.lean
@@ -4,6 +4,10 @@
 
 import logic.connectives.basic .inhabited
 
+using inhabited
+
+namespace nonempty
+
 inductive nonempty (A : Type) : Prop :=
 | nonempty_intro : A → nonempty A
 
@@ -12,3 +16,5 @@ nonempty_rec H2 H1
 
 theorem inhabited_imp_nonempty [instance] {A : Type} (H : inhabited A) : nonempty A :=
 nonempty_intro (default A)
+
+end nonempty
diff --git a/library/standard/logic/connectives/basic.lean b/library/standard/logic/connectives/basic.lean
index bcface38c..df02bf62f 100644
--- a/library/standard/logic/connectives/basic.lean
+++ b/library/standard/logic/connectives/basic.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.
 -- Authors: Leonardo de Moura, Jeremy Avigad
-----------------------------------------------------------------------------------------------------
 
 import general_notation .prop
 
@@ -57,6 +55,9 @@ assume Hna : ¬a, absurd (assume Ha : a, absurd_elim b Ha Hna) H
 theorem not_implies_right {a b : Prop} (H : ¬(a → b)) : ¬b :=
 assume Hb : b, absurd (assume Ha : a, Hb) H
 
+theorem contrapos {a b : Prop} (Hab : a → b) : (¬b → ¬a) :=
+assume Hnb Ha, Hnb (Hab Ha)
+
 
 -- and
 -- ---
diff --git a/library/standard/logic/connectives/cast.lean b/library/standard/logic/connectives/cast.lean
index de9831c90..a5c3aac52 100644
--- a/library/standard/logic/connectives/cast.lean
+++ b/library/standard/logic/connectives/cast.lean
@@ -6,7 +6,7 @@
 
 import .eq .quantifiers
 
-using eq_proofs
+using eq_ops
 
 definition cast {A B : Type} (H : A = B) (a : A) : B :=
 eq_rec a H
@@ -91,13 +91,13 @@ heq_to_eq (calc cast Hbc (cast Hab a)   == cast Hab a        : cast_heq Hbc (cas
                                    ...  == a                 : cast_heq Hab a
                                    ...  == cast (Hab ⬝ Hbc) a : hsymm (cast_heq (Hab ⬝ Hbc) a))
 
-theorem dcongr2 {A : Type} {B : A → Type} (f : Πx, B x) {a b : A} (H : a = b) : f a == f b :=
+theorem dcongr_arg {A : Type} {B : A → Type} (f : Πx, B x) {a b : A} (H : a = b) : f a == f b :=
 have e1 : ∀ (H : B a = B a), cast H (f a) = f a, from
   assume H, cast_eq H (f a),
 have e2 : ∀ (H : B a = B b), cast H (f a) = f b, from
   subst H e1,
-have e3 : cast (congr2 B H) (f a) = f b, from
-  e2 (congr2 B H),
+have e3 : cast (congr_arg B H) (f a) = f b, from
+  e2 (congr_arg B H),
 cast_eq_to_heq e3
 
 theorem pi_eq {A : Type} {B B' : A → Type} (H : B = B') : (Π x, B x) = (Π x, B' x) :=
@@ -106,20 +106,20 @@ subst H (refl (Π x, B x))
 theorem cast_app' {A : Type} {B B' : A → Type} (H : B = B') (f : Π x, B x) (a : A) :
   cast (pi_eq H) f a == f a :=
 have H1 : ∀ (H : (Π x, B x) = (Π x, B x)), cast H f a == f a, from
-  assume H, eq_to_heq (congr1 (cast_eq H f) a),
+  assume H, eq_to_heq (congr_fun (cast_eq H f) a),
 have H2 : ∀ (H : (Π x, B x) = (Π x, B' x)), cast H f a == f a, from
   subst H H1,
 H2 (pi_eq H)
 
 theorem cast_pull {A : Type} {B B' : A → Type} (H : B = B') (f : Π x, B x) (a : A) :
-                  cast (pi_eq H) f a = cast (congr1 H a) (f a) :=
+                  cast (pi_eq H) f a = cast (congr_fun H a) (f a) :=
 heq_to_eq (calc cast (pi_eq H) f a == f a                     : cast_app' H f a
-                             ...   == cast (congr1 H a) (f a) : hsymm (cast_heq (congr1 H a) (f a)))
+                             ...   == cast (congr_fun H a) (f a) : hsymm (cast_heq (congr_fun H a) (f a)))
 
-theorem hcongr1' {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A)
+theorem hcongr_fun' {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A)
     (H1 : f == f') (H2 : B = B')
   : f a == f' a :=
 heq_elim H1 (λ (Ht : (Π x, B x) = (Π x, B' x)) (Hw : cast Ht f = f'),
   calc f a == cast (pi_eq H2) f a  : hsymm (cast_app' H2 f a)
        ... =  cast Ht f a          : refl (cast Ht f a)
-       ... =  f' a                 : congr1 Hw a)
+       ... =  f' a                 : congr_fun Hw a)
diff --git a/library/standard/logic/connectives/eq.lean b/library/standard/logic/connectives/eq.lean
index 371a2f3eb..4a67c7f3f 100644
--- a/library/standard/logic/connectives/eq.lean
+++ b/library/standard/logic/connectives/eq.lean
@@ -54,27 +54,27 @@ theorem eq_rec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (
   from eq_rec_on H2 (take (H2 : b = b), eq_rec_on_id H2 _))
 H2
 
-namespace eq_proofs
+namespace eq_ops
   postfix `⁻¹`:100 := symm
   infixr `⬝`:75     := trans
   infixr `▸`:75    := subst
-end eq_proofs
-using eq_proofs
+end eq_ops
+using eq_ops
 
-theorem congr1 {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a :=
+theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a :=
 H ▸ refl (f a)
 
-theorem congr2 {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b :=
+theorem congr_arg {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b :=
 H ▸ refl (f a)
 
 theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b :=
 H1 ▸ H2 ▸ refl (f a)
 
 theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x :=
-take x, congr1 H x
+take x, congr_fun H x
 
 theorem not_congr {a b : Prop} (H : a = b) : (¬a) = (¬b) :=
-congr2 not H
+congr_arg not H
 
 theorem eqmp {a b : Prop} (H1 : a = b) (H2 : a) : b :=
 H1 ▸ H2
diff --git a/library/standard/logic/connectives/examples/instances_test.lean b/library/standard/logic/connectives/examples/instances_test.lean
index 80cc8e6bd..f14431fec 100644
--- a/library/standard/logic/connectives/examples/instances_test.lean
+++ b/library/standard/logic/connectives/examples/instances_test.lean
@@ -6,11 +6,12 @@ import ..instances
 
 using relation
 
+using relation.general_operations
+using relation.iff_ops
+using eq_ops
 
 section
 
-using relation.operations
-
 theorem test1 (a b : Prop) (H : a ↔ b) (H1 : a) : b := mp H H1
 
 end
@@ -18,10 +19,8 @@ end
 
 section
 
-using gensubst
-
 theorem test2 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
-subst H1 H2
+subst iff H1 H2
 
 theorem test3 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
 H1 ▸ H2
@@ -35,12 +34,16 @@ congr.infer iff iff (λa, (a ∨ c → ¬(d → a))) H1
 
 section
 
-using relation.symbols
-
 theorem test5 (T : Type) (a b c d : T) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
 H1 ⬝ H2⁻¹ ⬝ H3
 
 theorem test6 (a b c d : Prop) (H1 : a ↔ b) (H2 : c ↔ b) (H3 : c ↔ d) : a ↔ d :=
 H1 ⬝ (H2⁻¹ ⬝ H3)
 
+theorem test7 (T : Type) (a b c d : T) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
+trans H1 (trans (symm H2) H3)
+
+theorem test8 (a b c d : Prop) (H1 : a ↔ b) (H2 : c ↔ b) (H3 : c ↔ d) : a ↔ d :=
+trans iff H1 (trans iff (symm iff H2) H3)
+
 end
diff --git a/library/standard/logic/connectives/if.lean b/library/standard/logic/connectives/if.lean
index 765d4cb3d..4df01245d 100644
--- a/library/standard/logic/connectives/if.lean
+++ b/library/standard/logic/connectives/if.lean
@@ -5,7 +5,7 @@
 ----------------------------------------------------------------------------------------------------
 
 import logic.classes.decidable tools.tactic
-using decidable tactic eq_proofs
+using decidable tactic eq_ops
 
 definition ite (c : Prop) {H : decidable c} {A : Type} (t e : A) : A :=
 rec_on H (assume Hc,  t) (assume Hnc, e)
diff --git a/library/standard/logic/connectives/instances.lean b/library/standard/logic/connectives/instances.lean
index 20b73ee56..a39caa854 100644
--- a/library/standard/logic/connectives/instances.lean
+++ b/library/standard/logic/connectives/instances.lean
@@ -4,44 +4,46 @@
 
 import logic.connectives.basic logic.connectives.eq struc.relation
 
+namespace relation
+
 using relation
 
 -- Congruences for logic
 -- ---------------------
 
-theorem congr_not : congr.class iff iff not :=
-congr.mk
+theorem congr_not : congr iff iff not :=
+congr_mk
   (take a b,
     assume H : a ↔ b, iff_intro
       (assume H1 : ¬a, assume H2 : b, H1 (iff_elim_right H H2))
       (assume H1 : ¬b, assume H2 : a, H1 (iff_elim_left H H2)))
 
-theorem congr_and : congr.class2 iff iff iff and :=
-congr.mk2
+theorem congr_and : congr2 iff iff iff and :=
+congr2_mk
   (take a1 b1 a2 b2,
     assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2,
     iff_intro
       (assume H3 : a1 ∧ a2, and_imp_and H3 (iff_elim_left H1) (iff_elim_left H2))
       (assume H3 : b1 ∧ b2, and_imp_and H3 (iff_elim_right H1) (iff_elim_right H2)))
 
-theorem congr_or : congr.class2 iff iff iff or :=
-congr.mk2
+theorem congr_or : congr2 iff iff iff or :=
+congr2_mk
   (take a1 b1 a2 b2,
     assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2,
     iff_intro
       (assume H3 : a1 ∨ a2, or_imp_or H3 (iff_elim_left H1) (iff_elim_left H2))
       (assume H3 : b1 ∨ b2, or_imp_or H3 (iff_elim_right H1) (iff_elim_right H2)))
 
-theorem congr_imp : congr.class2 iff iff iff imp :=
-congr.mk2
+theorem congr_imp : congr2 iff iff iff imp :=
+congr2_mk
   (take a1 b1 a2 b2,
     assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2,
     iff_intro
       (assume H3 : a1 → a2, assume Hb1 : b1, iff_elim_left H2 (H3 ((iff_elim_right H1) Hb1)))
       (assume H3 : b1 → b2, assume Ha1 : a1, iff_elim_right H2 (H3 ((iff_elim_left H1) Ha1))))
 
-theorem congr_iff : congr.class2 iff iff iff iff :=
-congr.mk2
+theorem congr_iff : congr2 iff iff iff iff :=
+congr2_mk
   (take a1 b1 a2 b2,
     assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2,
     iff_intro
@@ -59,62 +61,87 @@ theorem congr_iff_compose [instance] := congr.compose21 congr_iff
 -- Generalized substitution
 -- ------------------------
 
-namespace gensubst
-
 -- TODO: note that the target has to be "iff". Otherwise, there is not enough
 -- information to infer an mp-like relation.
 
-theorem subst {T : Type} {R : T → T → Prop} {P : T → Prop} {C : congr.class R iff P}
+namespace general_operations
+
+theorem subst {T : Type} (R : T → T → Prop) ⦃P : T → Prop⦄ {C : congr R iff P}
   {a b : T} (H : R a b) (H1 : P a) : P b := iff_elim_left (congr.app C H) H1
 
-infixr `▸`:75    := subst
-
-end gensubst
-
+end general_operations
 
 -- = is an equivalence relation
 -- ----------------------------
 
-theorem is_reflexive_eq [instance] (T : Type) : relation.is_reflexive.class (@eq T) :=
-relation.is_reflexive.mk (@refl T)
+theorem is_reflexive_eq [instance] (T : Type) : relation.is_reflexive (@eq T) :=
+relation.is_reflexive_mk (@refl T)
 
-theorem is_symmetric_eq [instance] (T : Type) : relation.is_symmetric.class (@eq T) :=
-relation.is_symmetric.mk (@symm T)
+theorem is_symmetric_eq [instance] (T : Type) : relation.is_symmetric (@eq T) :=
+relation.is_symmetric_mk (@symm T)
 
-theorem is_transitive_eq [instance] (T : Type) : relation.is_transitive.class (@eq T) :=
-relation.is_transitive.mk (@trans T)
+theorem is_transitive_eq [instance] (T : Type) : relation.is_transitive (@eq T) :=
+relation.is_transitive_mk (@trans T)
+
+-- TODO: this is only temporary, needed to inform Lean that is_equivalence is a class
+theorem is_equivalence_eq [instance] (T : Type) : relation.is_equivalence (@eq T) :=
+relation.is_equivalence_mk _ _ _
 
 
 -- iff is an equivalence relation
 -- ------------------------------
 
-theorem is_reflexive_iff [instance] : relation.is_reflexive.class iff :=
-relation.is_reflexive.mk (@iff_refl)
+theorem is_reflexive_iff [instance] : relation.is_reflexive iff :=
+relation.is_reflexive_mk (@iff_refl)
 
-theorem is_symmetric_iff [instance] : relation.is_symmetric.class iff :=
-relation.is_symmetric.mk (@iff_symm)
+theorem is_symmetric_iff [instance] : relation.is_symmetric iff :=
+relation.is_symmetric_mk (@iff_symm)
 
-theorem is_transitive_iff [instance] : relation.is_transitive.class iff :=
-relation.is_transitive.mk (@iff_trans)
+theorem is_transitive_iff [instance] : relation.is_transitive iff :=
+relation.is_transitive_mk (@iff_trans)
 
 
 -- Mp-like for iff
 -- ---------------
 
-theorem mp_like_iff [instance] (a b : Prop) (H : a ↔ b) : relation.mp_like.class H :=
-relation.mp_like.mk (iff_elim_left H)
+theorem mp_like_iff [instance] (a b : Prop) (H : a ↔ b) : relation.mp_like H :=
+relation.mp_like_mk (iff_elim_left H)
+
+-- Substition for iff
+-- ------------------
+
+theorem subst_iff {P : Prop → Prop} {C : congr iff iff P} {a b : Prop} (H : a ↔ b) (H1 : P a) :
+  P b :=
+@general_operations.subst Prop iff P C a b H H1
+
+-- Support for calc
+-- ----------------
+
+calc_refl iff_refl
+calc_subst subst_iff
+calc_trans iff_trans
+
+namespace iff_ops
+  postfix `⁻¹`:100 := iff_symm
+  infixr `⬝`:75     := iff_trans
+  infixr `▸`:75    := subst_iff
+end iff_ops
+
+
+
 
 
 -- Boolean calculations
 -- --------------------
 
--- TODO: move these to new file
--- TODO: declare trans
+-- TODO: move these somewhere
 
 theorem or_right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b :=
 calc
   (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) : or_assoc _ _ _
-    ... ↔ a ∨ (c ∨ b) : congr.infer iff iff _ (or_comm b c)
-    ... ↔ (a ∨ c) ∨ b : iff_symm (or_assoc _ _ _)
+    ... ↔ a ∨ (c ∨ b) : {or_comm b c}
+     ... ↔ (a ∨ c) ∨ b : iff_symm (or_assoc _ _ _)
 
 -- TODO: add or_left_comm, and_right_comm, and_left_comm
+
+end relation
diff --git a/library/standard/logic/connectives/quantifiers.lean b/library/standard/logic/connectives/quantifiers.lean
index 960c0dc66..9eb3a3226 100644
--- a/library/standard/logic/connectives/quantifiers.lean
+++ b/library/standard/logic/connectives/quantifiers.lean
@@ -4,6 +4,8 @@
 
 import .basic .eq ..classes.nonempty
 
+using inhabited nonempty
+
 inductive Exists {A : Type} (P : A → Prop) : Prop :=
 | exists_intro : ∀ (a : A), P a → Exists P
 
@@ -52,12 +54,12 @@ theorem forall_true_iff_true (A : Type) : (∀x : A, true) ↔ true :=
 iff_intro (assume H, trivial) (assume H, take x, trivial)
 
 theorem forall_p_iff_p (A : Type) {H : inhabited A} (p : Prop) : (∀x : A, p) ↔ p :=
-iff_intro (assume Hl, inhabited_elim H (take x, Hl x)) (assume Hr, take x, Hr)
+iff_intro (assume Hl, inhabited_destruct H (take x, Hl x)) (assume Hr, take x, Hr)
 
 theorem exists_p_iff_p (A : Type) {H : inhabited A} (p : Prop) : (∃x : A, p) ↔ p :=
 iff_intro
   (assume Hl, obtain a Hp, from Hl, Hp)
-  (assume Hr, inhabited_elim H (take a, exists_intro a Hr))
+  (assume Hr, inhabited_destruct H (take a, exists_intro a Hr))
 
 theorem forall_and_distribute {A : Type} (φ ψ : A → Prop) : (∀x, φ x ∧ ψ x) ↔ (∀x, φ x) ∧ (∀x, ψ x) :=
 iff_intro
diff --git a/library/standard/struc/binary.lean b/library/standard/struc/binary.lean
index 98376edfc..a664b780c 100644
--- a/library/standard/struc/binary.lean
+++ b/library/standard/struc/binary.lean
@@ -5,7 +5,7 @@
 ----------------------------------------------------------------------------------------------------
 
 import logic.connectives.eq
-using eq_proofs
+using eq_ops
 
 namespace binary
 section
diff --git a/library/standard/struc/equivalence.lean b/library/standard/struc/equivalence.lean
deleted file mode 100644
index c87c12b14..000000000
--- a/library/standard/struc/equivalence.lean
+++ /dev/null
@@ -1,31 +0,0 @@
-----------------------------------------------------------------------------------------------------
--- 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.prop
-
-namespace equivalence
-section
-  parameter {A : Type}
-  parameter p : A → A → Prop
-  infix `∼`:50 := p
-  definition reflexive  := ∀a, a ∼ a
-  definition symmetric  := ∀a b, a ∼ b → b ∼ a
-  definition transitive := ∀a b c, a ∼ b → b ∼ c → a ∼ c
-end
-
-inductive equivalence {A : Type} (p : A → A → Prop) : Prop :=
-| equivalence_intro : reflexive p → symmetric p → transitive p → equivalence p
-
-theorem equivalence_reflexive [instance] {A : Type} {p : A → A → Prop} (H : equivalence p) : reflexive p :=
-equivalence_rec (λ r s t, r) H
-
-theorem equivalence_symmetric [instance] {A : Type} {p : A → A → Prop} (H : equivalence p) : symmetric p :=
-equivalence_rec (λ r s t, s) H
-
-theorem equivalence_transitive [instance] {A : Type} {p : A → A → Prop} (H : equivalence p) : transitive p :=
-equivalence_rec (λ r s t, t) H
-
-end equivalence
\ No newline at end of file
diff --git a/library/standard/struc/relation.lean b/library/standard/struc/relation.lean
index 1f02549f5..215b78a06 100644
--- a/library/standard/struc/relation.lean
+++ b/library/standard/struc/relation.lean
@@ -4,69 +4,72 @@
 
 import logic.connectives.prop
 
+
 -- General properties of relations
 -- -------------------------------
 
 namespace relation
 
 abbreviation reflexive {T : Type} (R : T → T → Type) : Type := ∀x, R x x
-abbreviation symmetric {T : Type} (R : T → T → Type) : Type := ∀x y, R x y → R y x
-abbreviation transitive {T : Type} (R : T → T → Type) : Type := ∀x y z, R x y → R y z → R x z
+abbreviation symmetric {T : Type} (R : T → T → Type) : Type := ∀⦃x y⦄, R x y → R y x
+abbreviation transitive {T : Type} (R : T → T → Type) : Type := ∀⦃x y z⦄, R x y → R y z → R x z
+
+
+inductive is_reflexive {T : Type} (R : T → T → Type) : Prop :=
+| is_reflexive_mk : reflexive R → is_reflexive R
 
 namespace is_reflexive
 
-  inductive class {T : Type} (R : T → T → Type) : Prop :=
-  | mk : reflexive R → class R
+  abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : is_reflexive R) : reflexive R :=
+  is_reflexive_rec (λu, u) C
 
-  abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : class R) : reflexive R :=
-  class_rec (λu, u) C
-
-  abbreviation infer ⦃T : Type⦄ {R : T → T → Type} {C : class R} : reflexive R :=
-  class_rec (λu, u) C
+  abbreviation infer ⦃T : Type⦄ (R : T → T → Type) {C : is_reflexive R} : reflexive R :=
+  is_reflexive_rec (λu, u) C
 
 end is_reflexive
 
+
+inductive is_symmetric {T : Type} (R : T → T → Type) : Prop :=
+| is_symmetric_mk : symmetric R → is_symmetric R
+
 namespace is_symmetric
 
-  inductive class {T : Type} (R : T → T → Type) : Prop :=
-  | mk : symmetric R → class R
+  abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : is_symmetric R) : symmetric R :=
+  is_symmetric_rec (λu, u) C
 
-  abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : class R) ⦃x y : T⦄ (H : R x y) : R y x :=
-  class_rec (λu, u) C x y H
-
-  abbreviation infer ⦃T : Type⦄ {R : T → T → Type} {C : class R} ⦃x y : T⦄ (H : R x y) : R y x :=
-  class_rec (λu, u) C x y H
+  abbreviation infer ⦃T : Type⦄ (R : T → T → Type) {C : is_symmetric R} : symmetric R :=
+  is_symmetric_rec (λu, u) C
 
 end is_symmetric
 
+
+inductive is_transitive {T : Type} (R : T → T → Type) : Prop :=
+| is_transitive_mk : transitive R → is_transitive R
+
 namespace is_transitive
 
-  inductive class {T : Type} (R : T → T → Type) : Prop :=
-  | mk : transitive R → class R
+  abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : is_transitive R) : transitive R :=
+  is_transitive_rec (λu, u) C
 
-  abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : class R) ⦃x y z : T⦄ (H1 : R x y)
-    (H2 : R y z) : R x z :=
-  class_rec (λu, u) C x y z H1 H2
-
-  abbreviation infer ⦃T : Type⦄ {R : T → T → Type} {C : class R} ⦃x y z : T⦄ (H1 : R x y)
-    (H2 : R y z) : R x z :=
-  class_rec (λu, u) C x y z H1 H2
+  abbreviation infer ⦃T : Type⦄ (R : T → T → Type) {C : is_transitive R} : transitive R :=
+  is_transitive_rec (λu, u) C
 
 end is_transitive
 
+
+inductive is_equivalence {T : Type} (R : T → T → Type) : Prop :=
+| is_equivalence_mk : is_reflexive R → is_symmetric R → is_transitive R → is_equivalence R
+
 namespace is_equivalence
 
-  inductive class {T : Type} (R : T → T → Type) : Prop :=
-  | mk : is_reflexive.class R → is_symmetric.class R → is_transitive.class R → class R
+  theorem is_reflexive {T : Type} (R : T → T → Type) {C : is_equivalence R} : is_reflexive R :=
+  is_equivalence_rec (λx y z, x) C
 
-  theorem is_reflexive {T : Type} {R : T → T → Type} {C : class R} : is_reflexive.class R :=
-  class_rec (λx y z, x) C
+  theorem is_symmetric {T : Type} {R : T → T → Type} {C : is_equivalence R} : is_symmetric R :=
+  is_equivalence_rec (λx y z, y) C
 
-  theorem is_symmetric {T : Type} {R : T → T → Type} {C : class R} : is_symmetric.class R :=
-  class_rec (λx y z, y) C
-
-  theorem is_transitive {T : Type} {R : T → T → Type} {C : class R} : is_transitive.class R :=
-  class_rec (λx y z, z) C
+  theorem is_transitive {T : Type} {R : T → T → Type} {C : is_equivalence R} : is_transitive R :=
+  is_equivalence_rec (λx y z, z) C
 
 end is_equivalence
 
@@ -74,112 +77,109 @@ instance is_equivalence.is_reflexive
 instance is_equivalence.is_symmetric
 instance is_equivalence.is_transitive
 
+
+-- partial equivalence relation
+inductive is_PER {T : Type} (R : T → T → Type) : Prop :=
+| is_PER_mk : is_symmetric R → is_transitive R → is_PER R
+
 namespace is_PER
 
-  inductive class {T : Type} (R : T → T → Type) : Prop :=
-  | mk : is_symmetric.class R → is_transitive.class R → class R
+  theorem is_symmetric {T : Type} {R : T → T → Type} {C : is_PER R} : is_symmetric R :=
+  is_PER_rec (λx y, x) C
 
-  theorem is_symmetric {T : Type} {R : T → T → Type} {C : class R} : is_symmetric.class R :=
-  class_rec (λx y, x) C
-
-  theorem is_transitive {T : Type} {R : T → T → Type} {C : class R} : is_transitive.class R :=
-  class_rec (λx y, y) C
+  theorem is_transitive {T : Type} {R : T → T → Type} {C : is_PER R} : is_transitive R :=
+  is_PER_rec (λx y, y) C
 
 end is_PER
 
--- instance is_PER.is_symmetric
+instance is_PER.is_symmetric
 instance is_PER.is_transitive
 
 
 -- Congruence for unary and binary functions
 -- -----------------------------------------
 
-namespace congr
-
-inductive class {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
+inductive congr {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
     (f : T1 → T2) : Prop :=
-| mk : (∀x y, R1 x y → R2 (f x) (f y)) → class R1 R2 f
-
-abbreviation app {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
-    {f : T1 → T2} (C : class R1 R2 f) ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
-class_rec (λu, u) C x y
-
-theorem infer {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
-    (f : T1 → T2) {C : class R1 R2 f} ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
-class_rec (λu, u) C x y
+| congr_mk : (∀x y, R1 x y → R2 (f x) (f y)) → congr R1 R2 f
 
 -- for binary functions
-inductive class2 {T1 : Type}  (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
+inductive congr2 {T1 : Type}  (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
     {T3 : Type} (R3 : T3 → T3 → Prop) (f : T1 → T2 → T3) : Prop :=
-| mk2 : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) →
-    class2 R1 R2 R3 f
+| congr2_mk : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) →
+    congr2 R1 R2 R3 f
 
-abbreviation app2 {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
-    {T3 : Type} {R3 : T3 → T3 → Prop}
-    {f : T1 → T2 → T3} (C : class2 R1 R2 R3 f) ⦃x1 y1 : T1⦄ ⦃x2 y2 : T2⦄
-  : R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2) :=
-class2_rec (λu, u) C x1 y1 x2 y2
+namespace congr
+
+  abbreviation app {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
+      {f : T1 → T2} (C : congr R1 R2 f) ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
+  congr_rec (λu, u) C x y
+
+  theorem infer {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
+      (f : T1 → T2) {C : congr R1 R2 f} ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
+  congr_rec (λu, u) C x y
+
+  abbreviation app2 {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
+      {T3 : Type} {R3 : T3 → T3 → Prop}
+      {f : T1 → T2 → T3} (C : congr2 R1 R2 R3 f) ⦃x1 y1 : T1⦄ ⦃x2 y2 : T2⦄ :
+    R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2) :=
+  congr2_rec (λu, u) C x1 y1 x2 y2
 
 -- ### general tools to build instances
 
-theorem compose
-    {T2 : Type} {R2 : T2 → T2 → Prop}
-    {T3 : Type} {R3 : T3 → T3 → Prop}
-    {g : T2 → T3} (C2 : congr.class R2 R3 g)
-    {{T1 : Type}} {R1 : T1 → T1 → Prop}
-    {f : T1 → T2} (C1 : congr.class R1 R2 f) :
-  congr.class R1 R3 (λx, g (f x)) :=
-mk (λx1 x2 H, app C2 (app C1 H))
+  theorem compose
+      {T2 : Type} {R2 : T2 → T2 → Prop}
+      {T3 : Type} {R3 : T3 → T3 → Prop}
+      {g : T2 → T3} (C2 : congr R2 R3 g)
+      ⦃T1 : Type⦄ {R1 : T1 → T1 → Prop}
+      {f : T1 → T2} (C1 : congr R1 R2 f) :
+    congr R1 R3 (λx, g (f x)) :=
+  congr_mk (λx1 x2 H, app C2 (app C1 H))
 
-theorem compose21
-    {T2 : Type} {R2 : T2 → T2 → Prop}
-    {T3 : Type} {R3 : T3 → T3 → Prop}
-    {T4 : Type} {R4 : T4 → T4 → Prop}
-    {g : T2 → T3 → T4} (C3 : congr.class2 R2 R3 R4 g)
-    ⦃T1 : Type⦄ {R1 : T1 → T1 → Prop}
-    {f1 : T1 → T2} (C1 : congr.class R1 R2 f1)
-    {f2 : T1 → T3} (C2 : congr.class R1 R3 f2) :
-  congr.class R1 R4 (λx, g (f1 x) (f2 x)) :=
-mk (λx1 x2 H, app2 C3 (app C1 H) (app C2 H))
+  theorem compose21
+      {T2 : Type} {R2 : T2 → T2 → Prop}
+      {T3 : Type} {R3 : T3 → T3 → Prop}
+      {T4 : Type} {R4 : T4 → T4 → Prop}
+      {g : T2 → T3 → T4} (C3 : congr2 R2 R3 R4 g)
+      ⦃T1 : Type⦄ {R1 : T1 → T1 → Prop}
+      {f1 : T1 → T2} (C1 : congr R1 R2 f1)
+      {f2 : T1 → T3} (C2 : congr R1 R3 f2) :
+    congr R1 R4 (λx, g (f1 x) (f2 x)) :=
+  congr_mk (λx1 x2 H, app2 C3 (app C1 H) (app C2 H))
 
-theorem const {T2 : Type} (R2 : T2 → T2 → Prop) (H : relation.reflexive R2)
-    ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
-  class R1 R2 (λu : T1, c) :=
-mk (λx y H1, H c)
+  theorem const {T2 : Type} (R2 : T2 → T2 → Prop) (H : relation.reflexive R2)
+      ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
+    congr R1 R2 (λu : T1, c) :=
+  congr_mk (λx y H1, H c)
 
 end congr
 
-end relation
-
-
--- TODO: notice these can't be in the congr namespace, if we want it visible without
+-- Notice these can't be in the congr namespace, if we want it visible without
 -- using congr.
 
 theorem congr_const [instance] {T2 : Type} (R2 : T2 → T2 → Prop)
-    {C : relation.is_reflexive.class R2} ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
-  relation.congr.class R1 R2 (λu : T1, c) :=
-relation.congr.const R2 (relation.is_reflexive.app C) R1 c
+    {C : is_reflexive R2} ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
+  congr R1 R2 (λu : T1, c) :=
+congr.const R2 (is_reflexive.app C) R1 c
 
 theorem congr_trivial [instance] {T : Type} (R : T → T → Prop) :
-  relation.congr.class R R (λu, u) :=
-relation.congr.mk (λx y H, H)
+  congr R R (λu, u) :=
+congr_mk (λx y H, H)
 
 
 -- Relations that can be coerced to functions / implications
 -- ---------------------------------------------------------
 
-namespace relation
+inductive mp_like {R : Type → Type → Prop} {a b : Type} (H : R a b) : Prop :=
+| mp_like_mk {} : (a → b) → @mp_like R a b H
 
 namespace mp_like
 
-inductive class {R : Type → Type → Prop} {a b : Type} (H : R a b) : Prop :=
-| mk {} : (a → b) → @class R a b H
+  definition app {R : Type → Type → Prop} {a : Type} {b : Type} {H : R a b}
+    (C : mp_like H) : a → b := mp_like_rec (λx, x) C
 
-definition app {R : Type → Type → Prop} {a : Type} {b : Type} {H : R a b}
-  (C : class H) : a → b := class_rec (λx, x) C
-
-definition infer ⦃R : Type → Type → Prop⦄ {a : Type} {b : Type} (H : R a b)
-  {C : class H} : a → b := class_rec (λx, x) C
+  definition infer ⦃R : Type → Type → Prop⦄ {a : Type} {b : Type} (H : R a b)
+    {C : mp_like H} : a → b := mp_like_rec (λx, x) C
 
 end mp_like
 
@@ -187,20 +187,21 @@ end mp_like
 -- Notation for operations on general symbols
 -- ------------------------------------------
 
-namespace operations
+namespace general_operations
 
+-- e.g. if R is an instance of the class, then "refl R" is reflexivity for the class
 definition refl := is_reflexive.infer
 definition symm := is_symmetric.infer
 definition trans := is_transitive.infer
 definition mp := mp_like.infer
 
-end operations
+end general_operations
 
-namespace symbols
+-- namespace
+--
+-- postfix `⁻¹`:100 := operations.symm
+-- infixr `⬝`:75     := operations.trans
 
-postfix `⁻¹`:100 := operations.symm
-infixr `⬝`:75     := operations.trans
-
-end symbols
+-- end symbols
 
 end relation
diff --git a/library/standard/tools/fake_simplifier.lean b/library/standard/tools/fake_simplifier.lean
new file mode 100644
index 000000000..28140299d
--- /dev/null
+++ b/library/standard/tools/fake_simplifier.lean
@@ -0,0 +1,9 @@
+import .tactic
+using tactic
+
+namespace fake_simplifier
+
+-- until we have the simplifier...
+definition simp : tactic := apply @sorry
+
+end fake_simplifier
diff --git a/library/standard/tools/tactic.lean b/library/standard/tools/tactic.lean
index 2bb013ad1..74e8de661 100644
--- a/library/standard/tools/tactic.lean
+++ b/library/standard/tools/tactic.lean
@@ -54,4 +54,5 @@ notation `?` t:max     := try t
 definition repeat1     (t : tactic) : tactic := t ; !t
 definition focus       (t : tactic) : tactic := focus_at t 0
 definition determ      (t : tactic) : tactic := at_most t 1
+
 end tactic