induction a with
| zero => exact h
| succ n' ih =>
 rw [←Nat.add_one, ←Nat.add_assoc, ←Nat.add_assoc, Nat.add_one, Nat.add_one]
 apply Nat.succ_lt_succ
 exact ih
a m n : Nat
h : m < n
⊢ m + a < n + a
no goals