proposition: Lemma A_plus_mult_distr_r m n p : m * (n + p) =A= m * n + m * p.
proof: Proof. rewrite Amult_comm, (Amult_comm m n), (Amult_comm m p). apply A_plus_mult_distr_l. Qed.
imports: Coq(Relations Arith Compare Bool Setoid Morphisms) CoLoR(RelDec LogicUtil RelExtras EqUtil NatUtil ZUtil)