p q : p * q~1 = p + (p * q)~0. Proof. induction p; simpl; trivial; f_ap. rewrite IHp. rewrite pos_add_assoc. rewrite (pos_add_comm q p). symmetry. apply pos_add_assoc. Qed.
Require Import Basics.Overture Basics.Tactics. Require Import Pos.Core.