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