case zero
n m : ℕ
k : Fin (zero + 1)
⊢ k ≤ k - 1 ↔ k = 0

case succ
n m n✝ : ℕ
k : Fin (Nat.succ n✝ + 1)
⊢ k ≤ k - 1 ↔ k = 0
n✝ m n : ℕ
k : Fin (n + 1)
⊢ k ≤ k - 1 ↔ k = 0
cases n
case succ
n m n✝ : ℕ
k : Fin (Nat.succ n✝ + 1)
⊢ k = k + 1 → k = 0
case succ
n m n✝ : ℕ
k : Fin (Nat.succ n✝ + 1)
⊢ k ≤ k - 1 ↔ k = 0
rw [← lt_sub_one_iff, le_iff_lt_or_eq, lt_sub_one_iff, or_iff_left_iff_imp, eq_comm,
  sub_eq_iff_eq_add]
no goals
case succ
n m n✝ : ℕ
k : Fin (Nat.succ n✝ + 1)
⊢ k = k + 1 → k = 0
simp
no goals
case zero
n m : ℕ
k : Fin (zero + 1)
⊢ k ≤ k - 1 ↔ k = 0
simp [fin_one_eq_zero k]