Fin.succ vs what I did

Stream: lean4

[Mark Santa Clara Munro]

I have been working on Gaussian Elimination and using Fin to do so. However, I feel like the way I did things could have been simplified. For example, I created a lemma:

/-- For any i : Fin m, if i + 1 is not equal to m, then i + 1 is strictly less than m. -/
lemma lessSucc {m : ℕ} (i : Fin m) (h : (i + 1: ℕ) ≠ m) : i + 1 < m := by
  omega

to use it in the function:

/-- Uses the pivot, located at row `p` and column `l` of matrix `M`, to turn the elements starting at row `i` into 0 below and going all the way down to the last row. This is done by adding row `p` of matrix `M` times scalar `-(M i l) * (1 / (M p l)` to row `i`. -/
def turnBelowIntoZero [DecidableEq α] [DivisionRing α] {m : ℕ} {n : ℕ}
    (M : Matrix (Fin m) (Fin n) α) (p : Fin m) (i : Fin m) (l : Fin n) :
    Matrix (Fin m) (Fin n) α :=
  if h1 : i + 1 = m then addMulRow M i p (-(M i l) * (1 / (M p l)))
  else
    let isucc := (⟨i+1, lessSucc i h1⟩ : Fin m)
    if M i l = 0 then turnBelowIntoZero M p isucc l
    else
      let M' := addMulRow M i p (-(M i l) * (1 / (M p l)))
      turnBelowIntoZero M' p isucc l
termination_by m - i

However, I find myself having to write a lot of have statements within proofs like the following have statements (please ignore the statement itself):

example {m : ℕ} (i : Fin m) (hi : ¬↑i + 1 = m) :
    i < i := by
  let isucc := (⟨i+1,lessSucc i hi⟩ : Fin m)
  have i_lt_isucc : i < isucc := by
    simp[isucc]
    fin_omega
  sorry

Is there a better way to go about things? I know there is Fin.succ, but since the bound on the result type is increased I don't think it would work. Hopefully I didn't make things too confusing but I am worried I should not be doing things like this for my theorems as I have so far, considering I am deep into the proofs of Gaussian Elimination.

[Jovan Gerbscheid]

You can also just use addition on Fin, i.e isucc := i+1

[Jovan Gerbscheid]

It's helpful if you write a #mwe that can be opened in the web editor and compiles there.