proposition: Lemma mul_xI_r p q : p * q~1 = p + (p * q)~0.
proof: 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.
imports: Basics.Overture Basics.Tactics Pos.Core