proposition: Lemma mul_lt_mono p q r s : p<q -> r<s -> p*r < q*s.
proof: Proof. intros. apply lt_trans with (p*s). - now apply mul_lt_mono_l. - now apply mul_lt_mono_r. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef