proposition: Lemma RS (SR : comSemiRingType) : @semi_ring_theory SR 0 1 +%R *%R eq.
proof: Proof. exact/mk_srt/mulrDl/mulrA/mulrC/mul0r/mul1r/addrA/addrC/add0r. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)