proposition: Lemma mul_compare_mono_r p q r : (q*p ?= r*p) = (q ?= r).
proof: Proof. rewrite 2 (mul_comm _ p). apply mul_compare_mono_l. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef