p q : p + q = q + p. Proof. revert q. induction p; destruct q; simpl; apply ap; trivial. rewrite 2 pos_add_carry_spec; by apply ap. Qed.
Require Import Basics.Overture Basics.Tactics. Require Import Pos.Core.