@soaproot This is a special case of the adjunction between rigs (+, ×, 0, 1) to rings (+, ×, -, 0, 1). You could formalize the fact that any rig R gives a ring R* such that R embeds into R* universally. I believe this is how Unimath library formalizes reals.