diff --git a/library/init/data/fin/basic.lean b/library/init/data/fin/basic.lean
index 673d1b6ca5..826500f7e1 100644
--- a/library/init/data/fin/basic.lean
+++ b/library/init/data/fin/basic.lean
@@ -47,6 +47,11 @@ lemma ne_of_vne {i j : fin n} (h : i.val ≠ j.val) : i ≠ j :=
 lemma vne_of_ne {i j : fin n} (h : i ≠ j) : i.val ≠ j.val :=
 λ h', absurd (eq_of_veq h') h
 
+protected def succ : fin n → fin (succ n)
+| ⟨a, h⟩ := ⟨nat.succ a, succ_le_succ h⟩
+
+instance : has_zero (fin (succ n)) := ⟨⟨0, succ_pos n⟩⟩
+
 end fin
 
 open fin
diff --git a/library/init/data/fin/default.lean b/library/init/data/fin/default.lean
index 582dedbc68..d3e08907ec 100644
--- a/library/init/data/fin/default.lean
+++ b/library/init/data/fin/default.lean
@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.data.fin.basic init.data.fin.ops
+import init.data.fin.basic
diff --git a/library/init/data/fin/ops.lean b/library/init/data/fin/ops.lean
deleted file mode 100644
index a2a6c20256..0000000000
--- a/library/init/data/fin/ops.lean
+++ /dev/null
@@ -1,104 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
--/
-prelude
-import init.data.nat init.data.fin.basic
-
-namespace fin
-open nat
-variable {n : nat}
-
-protected def succ : fin n → fin (succ n)
-| ⟨a, h⟩ := ⟨nat.succ a, succ_lt_succ h⟩
-
-def of_nat {n : nat} (a : nat) : fin (succ n) :=
-⟨a % succ n, nat.mod_lt _ (nat.zero_lt_succ _)⟩
-
-private lemma mlt {n b : nat} : ∀ {a}, n > a → b % n < n
-| 0     h := nat.mod_lt _ h
-| (a+1) h :=
-  have n > 0, from lt_trans (nat.zero_lt_succ _) h,
-  nat.mod_lt _ this
-
-protected def add : fin n → fin n → fin n
-| ⟨a, h⟩ ⟨b, _⟩ := ⟨(a + b) % n, mlt h⟩
-
-protected def mul : fin n → fin n → fin n
-| ⟨a, h⟩ ⟨b, _⟩ := ⟨(a * b) % n, mlt h⟩
-
-private lemma sublt {a b n : nat} (h : a < n) : a - b < n :=
-lt_of_le_of_lt (nat.sub_le a b) h
-
-protected def sub : fin n → fin n → fin n
-| ⟨a, h⟩ ⟨b, _⟩ := ⟨a - b, sublt h⟩
-
-private lemma modlt {a b n : nat} (h₁ : a < n) (h₂ : b < n) : a % b < n :=
-begin
-  cases b with b,
-  {simp [mod_zero], assumption},
-  {have h : a % (succ b) < succ b,
-   apply nat.mod_lt _ (nat.zero_lt_succ _),
-   exact lt_trans h h₂}
-end
-
-protected def mod : fin n → fin n → fin n
-| ⟨a, h₁⟩ ⟨b, h₂⟩ := ⟨a % b, modlt h₁ h₂⟩
-
-private lemma divlt {a b n : nat} (h : a < n) : a / b < n :=
-lt_of_le_of_lt (nat.div_le_self a b) h
-
-protected def div : fin n → fin n → fin n
-| ⟨a, h⟩ ⟨b, _⟩ := ⟨a / b, divlt h⟩
-
-instance : has_zero (fin (succ n)) := ⟨⟨0, succ_pos n⟩⟩
-instance : has_one (fin (succ n))  := ⟨of_nat 1⟩
-instance : has_add (fin n)         := ⟨fin.add⟩
-instance : has_sub (fin n)         := ⟨fin.sub⟩
-instance : has_mul (fin n)         := ⟨fin.mul⟩
-instance : has_mod (fin n)         := ⟨fin.mod⟩
-instance : has_div (fin n)         := ⟨fin.div⟩
-
-lemma of_nat_zero : @of_nat n 0 = 0 := rfl
-
-lemma add_def (a b : fin n) : (a + b).val = (a.val + b.val) % n :=
-show (fin.add a b).val = (a.val + b.val) % n, from
-by cases a; cases b; simp [fin.add]
-
-lemma mul_def (a b : fin n) : (a * b).val = (a.val * b.val) % n :=
-show (fin.mul a b).val = (a.val * b.val) % n, from
-by cases a; cases b; simp [fin.mul]
-
-lemma sub_def (a b : fin n) : (a - b).val = a.val - b.val :=
-show (fin.sub a b).val = a.val - b.val, from
-by cases a; cases b; simp [fin.sub]
-
-lemma mod_def (a b : fin n) : (a % b).val = a.val % b.val :=
-show (fin.mod a b).val = a.val % b.val, from
-by cases a; cases b; simp [fin.mod]
-
-lemma div_def (a b : fin n) : (a / b).val = a.val / b.val :=
-show (fin.div a b).val = a.val / b.val, from
-by cases a; cases b; simp [fin.div]
-
-lemma lt_def (a b : fin n) : (a < b) = (a.val < b.val) :=
-show (fin.lt a b) = (a.val < b.val), from
-by cases a; cases b; simp [fin.lt]
-
-lemma le_def (a b : fin n) : (a ≤ b) = (a.val ≤ b.val) :=
-show (fin.le a b) = (a.val ≤ b.val), from
-by cases a; cases b; simp [fin.le]
-
-lemma val_zero : (0 : fin (succ n)).val = 0 := rfl
-
-def pred {n : nat} : ∀ i : fin (succ n), i ≠ 0 → fin n
-| ⟨a, h₁⟩ h₂ := ⟨a.pred,
-  begin
-    have this : a ≠ 0,
-    { have aux₁ := vne_of_ne h₂,
-      dsimp at aux₁, rw val_zero at aux₁, exact aux₁ },
-    exact nat.pred_lt_pred this h₁
-  end⟩
-
-end fin
diff --git a/library/init/data/unsigned/basic.lean b/library/init/data/unsigned/basic.lean
index c070966bad..cd4367a2d7 100644
--- a/library/init/data/unsigned/basic.lean
+++ b/library/init/data/unsigned/basic.lean
@@ -20,6 +20,9 @@ zero_lt_succ _
 protected def of_nat' (n : nat) : unsigned :=
 if h : n < unsigned_sz then ⟨n, h⟩ else ⟨0, zero_lt_unsigned_sz⟩
 
+instance : has_zero unsigned := ⟨⟨0, succ_pos _⟩⟩
+instance : has_one unsigned  := ⟨⟨1, succ_le_succ (succ_pos _)⟩⟩
+
 def to_nat (c : unsigned) : nat := c.val
 
 end unsigned
diff --git a/library/init/data/unsigned/ops.lean b/library/init/data/unsigned/ops.lean
index 02c67e4f99..457d07d21c 100644
--- a/library/init/data/unsigned/ops.lean
+++ b/library/init/data/unsigned/ops.lean
@@ -4,17 +4,22 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.unsigned.basic init.data.fin.ops
+import init.data.unsigned.basic init.data.nat
 
 namespace unsigned
-def of_nat (n : nat) : unsigned := fin.of_nat n
-instance : has_zero unsigned := ⟨fin.of_nat 0⟩
-instance : has_one unsigned  := ⟨fin.of_nat 1⟩
-instance : has_add unsigned  := ⟨fin.add⟩
-instance : has_sub unsigned  := ⟨fin.sub⟩
-instance : has_mul unsigned  := ⟨fin.mul⟩
-instance : has_mod unsigned  := ⟨fin.mod⟩
-instance : has_div unsigned  := ⟨fin.div⟩
-instance : has_lt unsigned   := ⟨fin.lt⟩
-instance : has_le unsigned   := ⟨fin.le⟩
+
+def of_nat (n : nat) : unsigned :=
+⟨n % nat.succ _, nat.mod_lt _ (nat.zero_lt_succ _)⟩
+
+private lemma mlt {n b : nat} : ∀ {a}, n > a → b % n < n
+| 0     h := nat.mod_lt _ h
+| (a+1) h :=
+  have n > 0, from lt_trans (nat.zero_lt_succ _) h,
+  nat.mod_lt _ this
+
+protected def add : unsigned → unsigned → unsigned
+| ⟨a, h⟩ ⟨b, _⟩ := ⟨(a + b) % _, mlt h⟩
+
+instance : has_add unsigned := ⟨unsigned.add⟩
+
 end unsigned
diff --git a/tests/lean/397c.lean.expected.out b/tests/lean/397c.lean.expected.out
index 86ccb9f948..98ef0f2a7e 100644
--- a/tests/lean/397c.lean.expected.out
+++ b/tests/lean/397c.lean.expected.out
@@ -1,16 +1,14 @@
 [class_instances]  class-instance resolution trace
 [class_instances] (0) ?x_0 : has_one α := native.float.has_one
 failed is_def_eq
-[class_instances] (0) ?x_0 : has_one α := unsigned.has_one
-failed is_def_eq
-[class_instances] (0) ?x_0 : has_one α := @fin.has_one ?x_1
-failed is_def_eq
 [class_instances] (0) ?x_0 : has_one α := int.has_one
 failed is_def_eq
+[class_instances] (0) ?x_0 : has_one α := unsigned.has_one
+failed is_def_eq
 [class_instances] (0) ?x_0 : has_one α := nat.has_one
 failed is_def_eq
-[class_instances] (0) ?x_0 : has_one α := @ring.to_has_one ?x_2 ?x_3
-[class_instances] (1) ?x_3 : ring α := _inst_1
+[class_instances] (0) ?x_0 : has_one α := @ring.to_has_one ?x_1 ?x_2
+[class_instances] (1) ?x_2 : ring α := _inst_1
 [class_instances] caching instance for ring α
 _inst_1
 [class_instances] caching instance for has_one α
diff --git a/tests/lean/398c.lean.expected.out b/tests/lean/398c.lean.expected.out
index 87cecd6b9c..ac4cbdbeaf 100644
--- a/tests/lean/398c.lean.expected.out
+++ b/tests/lean/398c.lean.expected.out
@@ -1,16 +1,14 @@
 [class_instances]  class-instance resolution trace
 [class_instances] (0) ?x_0 : has_one α := native.float.has_one
 failed is_def_eq
-[class_instances] (0) ?x_0 : has_one α := unsigned.has_one
-failed is_def_eq
-[class_instances] (0) ?x_0 : has_one α := @fin.has_one ?x_1
-failed is_def_eq
 [class_instances] (0) ?x_0 : has_one α := int.has_one
 failed is_def_eq
+[class_instances] (0) ?x_0 : has_one α := unsigned.has_one
+failed is_def_eq
 [class_instances] (0) ?x_0 : has_one α := nat.has_one
 failed is_def_eq
-[class_instances] (0) ?x_0 : has_one α := @ring.to_has_one ?x_2 ?x_3
-[class_instances] (1) ?x_3 : ring α := _inst_1
+[class_instances] (0) ?x_0 : has_one α := @ring.to_has_one ?x_1 ?x_2
+[class_instances] (1) ?x_2 : ring α := _inst_1
 [class_instances] caching instance for ring α
 _inst_1
 [class_instances] caching instance for has_one α
diff --git a/tests/lean/run/array1.lean b/tests/lean/run/array1.lean
index c1d75e923d..ee6c3bd3ef 100644
--- a/tests/lean/run/array1.lean
+++ b/tests/lean/run/array1.lean
@@ -24,5 +24,5 @@ a^.foldl 0 (+)
 #eval array_sum (mk_array 10 1)
 
 #eval (mk_array 10 1)^.data ⟨1, dec_trivial⟩ + 20
-#eval (mk_array 10 1)^.data 2
-#eval (mk_array 10 3)^.data 2
+#eval (mk_array 10 1)^.data ⟨2, dec_trivial⟩
+#eval (mk_array 10 3)^.data ⟨2, dec_trivial⟩
diff --git a/tests/lean/tc_caching.lean.expected.out b/tests/lean/tc_caching.lean.expected.out
index 24f5c53c99..d7e28dfac2 100644
--- a/tests/lean/tc_caching.lean.expected.out
+++ b/tests/lean/tc_caching.lean.expected.out
@@ -29,12 +29,10 @@
 [class_instances]  class-instance resolution trace
 [class_instances] (0) ?x_0 : has_one ℕ := native.float.has_one
 failed is_def_eq
-[class_instances] (0) ?x_0 : has_one ℕ := unsigned.has_one
-failed is_def_eq
-[class_instances] (0) ?x_0 : has_one ℕ := @fin.has_one ?x_1
-failed is_def_eq
 [class_instances] (0) ?x_0 : has_one ℕ := int.has_one
 failed is_def_eq
+[class_instances] (0) ?x_0 : has_one ℕ := unsigned.has_one
+failed is_def_eq
 [class_instances] (0) ?x_0 : has_one ℕ := nat.has_one
 [class_instances] caching instance for has_one ℕ
 nat.has_one
@@ -50,8 +48,6 @@ nat.has_one
 failed is_def_eq
 [class_instances] (0) ?x_0 : has_add ℕ := unsigned.has_add
 failed is_def_eq
-[class_instances] (0) ?x_0 : has_add ℕ := @fin.has_add ?x_1
-failed is_def_eq
 [class_instances] (0) ?x_0 : has_add ℕ := int.has_add
 failed is_def_eq
 [class_instances] (0) ?x_0 : has_add ℕ := options.has_add