proposition: Theorem Pmult_nat_l_plus_morphism : forall p q n, Pmult_nat (p + q) n = Pmult_nat p n + Pmult_nat q n.
proof: Proof. intros. rewrite !Pmult_nat_mult, Pos2Nat.inj_add. apply Nat.mul_add_distr_r. Qed.
imports: BinPos PeanoNat