From 0ac414aff5cb39f286ff34787fd650b7eb5dc135 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 27 Nov 2020 11:58:59 +0000
Subject: [PATCH] feat(data/fin): Add pred_{le,lt}_pred_iff (#5121)

---
 src/data/fin.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/data/fin.lean b/src/data/fin.lean
index 17e9ed66b6be7..f9f6298fa4bb4 100644
--- a/src/data/fin.lean
+++ b/src/data/fin.lean
@@ -304,6 +304,14 @@ by { cases i, refl }
   fin.pred ⟨i + 1, add_lt_add_right h 1⟩ (ne_of_vne (ne_of_gt (mk_succ_pos i h))) = ⟨i, h⟩ :=
 by simp only [ext_iff, coe_pred, coe_mk, nat.add_sub_cancel]
 
+@[simp] lemma pred_le_pred_iff {n : ℕ} {a b : fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :
+  a.pred ha ≤ b.pred hb ↔ a ≤ b :=
+by rw [←succ_le_succ_iff, succ_pred, succ_pred]
+
+@[simp] lemma pred_lt_pred_iff {n : ℕ} {a b : fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :
+  a.pred ha < b.pred hb ↔ a < b :=
+by rw [←succ_lt_succ_iff, succ_pred, succ_pred]
+
 @[simp] lemma pred_inj :
   ∀ {a b : fin (n + 1)} {ha : a ≠ 0} {hb : b ≠ 0}, a.pred ha = b.pred hb ↔ a = b
 | ⟨0,   _⟩  b         ha hb := by contradiction