@SemiRing R Re Rplus Rmult Rzero Rone. Proof. repeat (constructor; try assumption); repeat intro ; unfold equiv, mon_unit, sg_op, zero_is_mon_unit, plus_is_sg_op, one_is_mon_unit, mult_is_sg_op, zero, mult, plus; ring. Qed.
Require Import Require Import