proposition: Lemma divide_mul_r p q r : (p|r) -> (p|q*r).
proof: Proof. rewrite mul_comm. apply divide_mul_l. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef