axiom Rplus_commutative: ∀x,y:R. (j ? x) + (j ? y) ≡ (j ? y) + (j ? x).
axiom R0_neutral: ∀x:R. (j ? x) + (j ? R0) ≡ (j ? x).
axiom Rplus_commutative: ∀x,y:R. (j ? x) + (j ? y) ≡ (j ? y) + (j ? x).
axiom R0_neutral: ∀x:R. (j ? x) + (j ? R0) ≡ (j ? x).