p q r : p * (q + r) = p * q + p * r. Proof. induction p; cbn; [reflexivity | f_ap | ]. rewrite IHp. set (m:=(p*q)~0). set (n:=(p*r)~0). change ((p*q+p*r)~0) with (m+n). rewrite 2 pos_add_assoc; f_ap. rewrite <- 2 pos_add_assoc; f_ap. apply pos_add_comm. Qed.
Require Import Basics.Overture Basics.Tactics. Require Import Pos.Core.