rw [←Nat.add_one, ←Nat.add_assoc, ←Nat.add_assoc, Nat.add_one, Nat.add_one]
case succ
m n : Nat
h : m < n
n' : Nat
ih : m + n' < n + n'
⊢ m + succ n' < n + succ n'
case succ
m n : Nat
h : m < n
n' : Nat
ih : m + n' < n + n'
⊢ succ (m + n') < succ (n + n')