> Are you sure that the assumptions that your proof relies on are more fundamental than than what you are trying to prove?

Yes, at least to the extent that "fundamental-ness" can be defined. It is a well, and probably universally, established convention that the field axioms allowing division by non-0 elements (that is to say, allowing multiplication by arbitrary elements, and multiplicative inversion of non-0 elements) is taken as part of the definition of a field, and the fact that the set of non-0 elements in a field is closed under multiplication as a theorem about fields.

I believe the point the person you were responding to was getting at is that the person's proof assumes that the reals are a field. It's not a convention that cancellation holds for fields. It's a theorem one proves about integral domains. That a field is closed under multiplication is not a theorem; it's part of the definition of being a ring.

> It's not a convention that cancellation holds for fields. It's a theorem one proves about integral domains. That a field is closed under multiplication is not a theorem; it's part of the definition of being a ring.

Yes, that's what I said. My point was that, between

(A) making an axiom the right to divide in a field by non-0 numbers, and proving the closure of non-0 numbers in a field under multiplication,

and

(B) just making an axiom the closure of non-0 numbers in a field under multiplication,

it is only convention (rooted in the deeper convention of not making an additional axiom out of something we could prove from existing ones) that we choose (A) instead of (B). (Also notice that I was talking about the closure under multiplication of the set of non-0 numbers, which is (usually) not part of the definition, rather than of the entire set, which is indeed always part of the definition.)