cases a with
| ofNat x => simp only [modToNat_ofNat, x.mod_lt (n.succ_pos)]
| negSucc x =>
  let y := x % n.succ
  have : n.succ - y - 1 ≤ n := by
    have : n.succ - y - 1 = n - y := n.add_sub_add_right 1 y
    rw [this]
    exact n.sub_le y
  exact Nat.lt_succ_of_le this
a : Int
n : Nat
⊢ modToNat a (succ n) < succ n
no goals