How to prove $c = a + b$ using Program Verification Techniques

Question

I am trying to prove an elementary thing, but it seems at some point you get down to atoms where you can't prove anything else. This is why I am wondering about proving $c = a + b$, it seems like an atom.

\begin{align} \{a, b\}\\ c = a + b\\ \{a, b, c = a + b\} \end{align}

This is my attempt at a Hoare assertion. It says "given $a$ and $b$, if I assign $c$ to $a + b$, then I end up with $a$ and $b$ unchanged, and $c$ assigned to $a + b$." That is, it's saying "if I do $c = a + b$, then I end up with $c = a + b$," which feels reduntant. In addition, this seems hard to formalize in programming. If the form is $\{P_1\}\ Q\ \{P_2\}$, then $Q$ and the $c$ part of $P_2$ is the same code, namely $c = a + b$. So I don't see there being any need to write an assertion for addition, we can just state it's properties (that it returns a number) and it is proven by definition. That is, it's an axiom.

Wondering if this is true, or where I am missing something. Because when I tried writing this out in software I end up with basically what it looks like in that definition of the Hoare assertion above, $c = a + b$ twice.