simp [add, mul, ih]
case succ
l m n' : ℕ
ih : mul l (add m n') = add (mul l m) (mul l n')
⊢ mul l (add m (Nat.succ n')) = add (mul l m) (mul l (Nat.succ n'))
case succ
l m n' : ℕ
ih : mul l (add m n') = add (mul l m) (mul l n')
⊢ add l (add (mul l m) (mul l n')) = add (mul l m) (add l (mul l n'))