proposition: Lemma ZType_two_2 : two = 2.
proof: Proof. unfold_equiv. rewrite spec_2. now rewrite rings.preserves_plus, rings.preserves_1. 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