diff --git a/library/init/data/fin/basic.lean b/library/init/data/fin/basic.lean
index cea8d99ada..df46273fe6 100644
--- a/library/init/data/fin/basic.lean
+++ b/library/init/data/fin/basic.lean
@@ -47,15 +47,15 @@ protected def add : fin n → fin n → fin n
 protected def mul : fin n → fin n → fin n
 | ⟨a, h⟩ ⟨b, _⟩ := ⟨(a * b) % n, mlt h⟩
 
+protected def sub : fin n → fin n → fin n
+| ⟨a, h⟩ ⟨b, _⟩ := ⟨(a + (n - b)) % n, mlt h⟩
+
 /-
 Remark: sub/mod/div can be defined without using (% n), but
 we are trying to minimize the number of nat theorems
 needed to boostrap Lean.
 -/
 
-protected def sub : fin n → fin n → fin n
-| ⟨a, h⟩ ⟨b, _⟩ := ⟨(a - b) % n, mlt h⟩
-
 protected def mod : fin n → fin n → fin n
 | ⟨a, h⟩ ⟨b, _⟩ := ⟨(a % b) % n, mlt h⟩
 
diff --git a/library/init/data/repr.lean b/library/init/data/repr.lean
index 2fabbaf741..955d83d72b 100644
--- a/library/init/data/repr.lean
+++ b/library/init/data/repr.lean
@@ -128,6 +128,9 @@ instance : has_repr string :=
 instance (n : nat) : has_repr (fin n) :=
 ⟨λ f, repr (fin.val f)⟩
 
+instance : has_repr uint16 :=
+⟨λ n, repr (fin.val n)⟩
+
 instance : has_repr uint32 :=
 ⟨λ n, repr (fin.val n)⟩
 
diff --git a/library/init/data/to_string.lean b/library/init/data/to_string.lean
index 7b7c0c697e..492df8aa87 100644
--- a/library/init/data/to_string.lean
+++ b/library/init/data/to_string.lean
@@ -51,6 +51,9 @@ instance : has_to_string char :=
 instance (n : nat) : has_to_string (fin n) :=
 ⟨λ f, to_string (fin.val f)⟩
 
+instance : has_to_string uint16 :=
+⟨λ n, to_string (fin.val n)⟩
+
 instance : has_to_string uint32 :=
 ⟨λ n, to_string (fin.val n)⟩
 
diff --git a/library/init/data/uint.lean b/library/init/data/uint.lean
index 8ef538f913..9f909146fa 100644
--- a/library/init/data/uint.lean
+++ b/library/init/data/uint.lean
@@ -7,12 +7,19 @@ prelude
 import init.data.fin.basic
 
 open nat
+def uint16_sz : nat := 65536
+def uint16 := fin uint16_sz
+
 def uint32_sz : nat := 4294967296
 def uint32 := fin uint32_sz
 
 def uint64_sz : nat := 18446744073709551616
 def uint64 := fin uint64_sz
 
+instance : decidable_eq uint16 :=
+have decidable_eq (fin uint16_sz), from fin.decidable_eq _,
+this
+
 instance : decidable_eq uint32 :=
 have decidable_eq (fin uint32_sz), from fin.decidable_eq _,
 this
@@ -21,6 +28,16 @@ instance : decidable_eq uint64 :=
 have decidable_eq (fin uint64_sz), from fin.decidable_eq _,
 this
 
+instance : has_zero uint16 := ⟨fin.of_nat 0⟩
+instance : has_one uint16  := ⟨fin.of_nat 1⟩
+instance : has_add uint16  := ⟨fin.add⟩
+instance : has_sub uint16  := ⟨fin.sub⟩
+instance : has_mul uint16  := ⟨fin.mul⟩
+instance : has_mod uint16  := ⟨fin.mod⟩
+instance : has_div uint16  := ⟨fin.div⟩
+instance : has_lt uint16   := ⟨fin.lt⟩
+instance : has_le uint16   := ⟨fin.le⟩
+
 instance : has_zero uint32 := ⟨fin.of_nat 0⟩
 instance : has_one uint32  := ⟨fin.of_nat 1⟩
 instance : has_add uint32  := ⟨fin.add⟩
@@ -41,6 +58,12 @@ instance : has_div uint64  := ⟨fin.div⟩
 instance : has_lt uint64   := ⟨fin.lt⟩
 instance : has_le uint64   := ⟨fin.le⟩
 
+def uint16.of_nat (n : nat) : uint16 :=
+fin.of_nat n
+
+def uint16.to_nat (u : uint16) : nat :=
+fin.val u
+
 def uint32.of_nat (n : nat) : uint32 :=
 fin.of_nat n