I’d cavil a bit about the presentation.
(ℓ+m)+n=ℓ+(m+n) rather than
(ℓ+m)=n=ℓ+(m+n).
The latter statement is not generally true. For example, 3 + 5 = 8, but 8 does not equal 3 + (5 + 8).
Ignoring what is almost certainly a typo, I find the presentation weird. You develop a base case of
(ℓ+m)+1=ℓ+(m+1). But then you seemingly ignore it.
(ℓ+m)+(n+1)=(ℓ+m)+s(n)=s{(ℓ+m)+n}.
Good so far.
But then you go
s{(ℓ+m)+n}=s{ℓ+(m+n)},
WHICH IS ASSUMING THAT WHICH IS TO BE PROVED.
This is partly a presentation issue of letting variable names jump around. So we show that
(a+b)+1=a+(b+1). Then, we letk be an arbitrary natural number such that (ℓ+m)+k=ℓ+(m+k).(ℓ+m)+(k+1)=(ℓ+m)+s(k) by definition of successor.∴(ℓ+m)+(k+1)=s{(ℓ+m)+k)} by Axiom 2.∴(ℓ+m)+(k+1)=s{ℓ+(m+k)} by definition of k.∴(ℓ+m)+(k+1)={ℓ+(m+k)}+1 by definition of successor.∴(ℓ+m)+(k+1)=ℓ+{(m+k)+1} ∵ (a+b)+1=a+(b+1).∴(ℓ+m)+(k+1)=ℓ+{m+(k+1)} ∵ (a+b)+1=a+(b+1).Thus, by induction, (ℓ+m)+n=ℓ+(m+n) for all natural numbers ℓ, m, and m.
It has been well over 50 years since I studied the use of the Peano Postulates, but my recollection is that you needed to be beyond meticulous. I believe you had the proof in your mind, but I am not satisfied that your presentation will pass muster. But maybe I am just an old fuss-budget.