no goals
n m i : ℕ
h : i < n + 1
⊢ pred { val := i + 1, isLt := (_ : i + 1 < n + 1 + 1) } (_ : { val := i + 1, isLt := (_ : i + 1 < n + 1 + 1) } ≠ 0) =
    { val := i, isLt := h }
simp only [ext_iff, coe_pred, add_tsub_cancel_right]