proposition: Lemma stdlib_ring_theory R `{Ring R} : Ring_theory.ring_theory 0 1 (+) (.*.) (λ x y, x - y) (-) (=).
proof: Proof. constructor; intros. apply left_identity. apply commutativity. apply associativity. apply left_identity. apply commutativity. apply associativity. rewrite commutativity, distribute_l. now setoid_rewrite commutativity at 2 3. reflexivity. apply (right_inverse x). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra