proposition: Lemma ZType_succ_1_plus x : succ x = 1 + x.
proof: Proof. unfold_equiv. rewrite spec_succ, rings.preserves_plus, rings.preserves_1. now rewrite commutativity. 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