proposition: Lemma mul_le_mono_l p q r : q<=r <-> p*q<=p*r.
proof: Proof. unfold le. rewrite mul_compare_mono_l. apply iff_refl. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef