diff --git a/library/init/data/fin/ops.lean b/library/init/data/fin/ops.lean
index 68b5863665..cedd522322 100644
--- a/library/init/data/fin/ops.lean
+++ b/library/init/data/fin/ops.lean
@@ -99,4 +99,16 @@ 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 :=
+begin unfold has_zero.zero of_nat, dsimp, rw zero_mod end
+
+def pred {n : nat} : ∀ i : fin (succ n), i ≠ 0 → fin n
+| ⟨a, h₁⟩ h₂ := ⟨a.pred,
+  begin
+    assert this : a ≠ 0,
+    { note aux₁ := vne_of_ne h₂,
+      dsimp at aux₁, rw val_zero at aux₁, exact aux₁ },
+    exact nat.pred_lt_pred this (nat.succ_ne_zero n) h₁
+  end⟩
+
 end fin
diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean
index d895324fe0..de9378dbce 100644
--- a/library/init/data/nat/lemmas.lean
+++ b/library/init/data/nat/lemmas.lean
@@ -253,6 +253,11 @@ le_of_succ_le
 lemma lt_of_succ_lt_succ {a b : ℕ} : succ a < succ b → a < b :=
 le_of_succ_le_succ
 
+lemma pred_lt_pred : ∀ {n m : ℕ}, n ≠ 0 → m ≠ 0 → n < m → pred n < pred m
+| 0         _       h₁ h₂ h := absurd rfl h₁
+| _         0       h₁ h₂ h := absurd rfl h₂
+| (succ n) (succ m) _  _  h := lt_of_succ_lt_succ h
+
 protected lemma lt_or_ge : ∀ (a b : ℕ), a < b ∨ a ≥ b
 | a 0     := or.inr (zero_le a)
 | a (b+1) :=