\forall inv1: (\forall x:A. (add x (inv x)) = one).
\forall inv2: (\forall x:A. (mult x (inv x)) = zero).
\forall x,y:A. (add (inv x) (mult y x)) = (add (inv x) y).
\forall inv1: (\forall x:A. (add x (inv x)) = one).
\forall inv2: (\forall x:A. (mult x (inv x)) = zero).
\forall x,y:A. (add (inv x) (mult y x)) = (add (inv x) y).