Here's the field proof I'm pulling out of memeory:
x*0 = x*(y + -y) = x*y + x*(-y) = x*y - x*y = 0
This relies on the existence of additive inverses for the first step, distribution in the second step, and the fact that x(-y) = -(xy) in the third step. That third property can be derived from sufficiently-specific ring axioms, but I forget how specific they have to be. It might be true in any ring by virtue of distribution but I forget the proof.So to answer your question, yes there are... but it depends on the context. In some situations it may need to be axiomatic. A recursively-defined system like Peano may need to take it axiomatically as a base case.
Cancellation yields 0=xy+x(-y)
Therefore -(xy)=x(-y)
1) From the equation x0 + x0 = x0, you don't need inverses, just cancellation. I believe that cancellation is a strictly weaker property.
2) From the equation x0 + x0 = x0, note that x0 is the additive identity. Inverses are unique, thus x0 = 0.
Unfortunately, I'm not familiar enough with Peano arithmetic to know if proving either of these statements requires the statement we're trying to prove, that x*0 = 0. I'm more familiar with algebra, where inverses exist axiomatically. But at least we've weakened the hypotheses!
a*0 = 0
a*S(b) = a*b+a
Cancellation follows from injectivity of S by induction.