axiom Rmult_assoc: associative ? Rmult.
axiom Rmult_comm: symmetric ? Rmult.
axiom Rmult_Rplus_distr: distributive ? Rmult Rplus.
axiom Rmult_assoc: associative ? Rmult.
axiom Rmult_comm: symmetric ? Rmult.
axiom Rmult_Rplus_distr: distributive ? Rmult Rplus.