I am trying to prove lemma mod_pres_succ {m n} (h : (m + 1) % n ≠ 0) : m % n + 1 = (m + 1) % n.

I have started with cases (@trichotomous _ (<) _ m n) with h₁ h₂, where I can show m < n and m = n. However, in the m > n case (where modulus is overflown), I am stuck. I tried by induction on m, where the base case is trivial, but the inductive step is in the following state:

n m : ℕ,
ih : (m + 1) % n ≠ 0 → n < m → m % n + 1 = (m + 1) % n,
h : (m + 1 + 1) % n ≠ 0,
h₃ : n < m + 1
⊢ (m + 1) % n + 1 = (m + 1 + 1) % n

How can I proceed?

Note: Here's the entire (incomplete) proof where I admitted some parts to make it short.

lemma mod_pres_succ {m n} (h : (m + 1) % n ≠ 0) : m % n + 1 = (m + 1) % n :=
begin
  cases (@trichotomous _ (<) _ m n) with h₁ h₂,
    {admit}, -- this I can show
    {
      cases h₂ with h₂ h₃,
        {admit}, -- this I can show
        {
          induction m with m ih,
            {cases h₃},
            {
              rw nat.succ_eq_add_one at *,
              -- Completely stuck besides a random rw ← ih
            }
        }
    }
end