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