proposition: Lemma ZType_ring_theory: ring_theory zero one add mul sub opp eq.
proof: Proof. repeat split; repeat intro; axioms.zify; auto with zarith. Qed.
imports: Bignums.SpecViaZ.ZSig Bignums.SpecViaZ.ZSigZAxioms Coq.NArith.NArith Coq.ZArith.ZArith MathClasses.implementations.nonneg_integers_naturals MathClasses.interfaces.orders MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.additional_operations