proposition: Lemma stdlib_semiring_theory R `{SemiRing R} : Ring_theory.semi_ring_theory 0 1 (+) (.*.) (=).
proof: Proof. constructor; intros. apply left_identity. apply commutativity. apply associativity. apply left_identity. apply left_absorb. apply commutativity. apply associativity. rewrite commutativity, distribute_l. now setoid_rewrite commutativity at 2 3. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra