proposition: Lemma abs_succ_neg : forall p, Z.abs_nat (Z.succ (Z.neg p)) = Nat.pred (Pos.to_nat p).
proof: Proof. move => p. destruct p using Pos.peano_ind. reflexivity. rewrite -neg_pred /Z.abs_nat. rewrite Pos2Nat.inj_pred. reflexivity. apply Pos.lt_1_succ. apply Pos.lt_gt; apply Pos.lt_1_succ. Qed.
imports: Coq(Arith Basics List Recdef ZArith Lia) mathcomp(ssrbool ssreflect ssrnat) QuickChick(Classes Sets Producer Enumerators Generators Tactics)