Library Coq.setoid_ring.Ring_base



Require Export Ring_theory.
Require Export Ring_tac.
Require Import InitialRing.