proposition: Lemma neg_pred : forall p, (p > 1)%positive -> Z.neg (Pos.pred p) = Z.succ (Z.neg p).
proof: Proof. move => p Hp. destruct p using Pos.peano_ind. by inversion Hp. rewrite Pos.pred_succ. rewrite neg_succ. rewrite Z.succ_pred. reflexivity. Qed.
imports: Coq(Arith Basics List Recdef ZArith Lia) mathcomp(ssrbool ssreflect ssrnat) QuickChick(Classes Sets Producer Enumerators Generators Tactics)