proposition: Lemma abs_div2_pos : forall p, Z.abs_nat (Z.div2 (Z.pos p)) = Nat.div2 (Pos.to_nat p).
proof: Proof. intros. destruct p. rewrite /Z.div2 /Pos.div2. rewrite /Z.abs_nat. rewrite Pos2Nat.inj_xI. rewrite <- Nat.add_1_r. rewrite Nat.mul_comm. rewrite Nat.div2_div. rewrite Nat.div_add_l; simpl; lia. rewrite /Z.div2 /Pos.div2. rewrite /Z.abs_nat. rewrite Pos2Nat.inj_xO. rewrite Nat.mul_comm. rewrite Nat.div2_div. rewrite Nat.div_mul. reflexivity. lia. reflexivity. Qed.
imports: Coq(Arith Basics List Recdef ZArith Lia) mathcomp(ssrbool ssreflect ssrnat) QuickChick(Classes Sets Producer Enumerators Generators Tactics)