proposition: Lemma neg_succ : forall p, Z.neg (Pos.succ p) = Z.pred (Z.neg p).
proof: Proof. move => p. rewrite <- Pos.add_1_r. rewrite <- Pos2Z.add_neg_neg. rewrite <- Z.sub_1_r. reflexivity. Qed.
imports: Coq(Arith Basics List Recdef ZArith Lia) mathcomp(ssrbool ssreflect ssrnat) QuickChick(Classes Sets Producer Enumerators Generators Tactics)