p q : p + pos_succ q = pos_succ (p + q). Proof. revert q. induction p; destruct q; simpl; apply ap; auto using pos_add_1_r; rewrite pos_add_carry_spec; auto. Qed.
Require Import Basics.Overture Basics.Tactics. Require Import Pos.Core.