proposition: Theorem mul_add_distr_r p q r : (p + q) * r = p * r + q * r.
proof: Proof. rewrite 3 (mul_comm _ r); apply mul_add_distr_l. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef