proposition: Theorem pos_mul_add_distr_l p q r : p * (q + r) = p * q + p * r.
proof: 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.
imports: Basics.Overture Basics.Tactics Pos.Core