[mfukar]

a = a (equality is reflexive under Peano arithmetic)

=> a + c = a + c (addition is commutative under Peano arithmetic)

=> a + c = b + c (a == b)

=> a + c = b + d (c == d)

qed