no goals
n✝ m n : ℕ
i : Fin (n + 1)
hi : i ≠ 0
j : Fin n
h : pred i hi = j
⊢ i = succ j
simp only [← h, Fin.succ_pred]
no goals
n✝ m n : ℕ
i : Fin (n + 1)
hi : i ≠ 0
j : Fin n
h : i = succ j
⊢ pred i hi = j
simp only [h, Fin.pred_succ]