proposition: Lemma Qmult_lt_r: forall x y z, 0 < z -> (x*z < y*z <-> x < y).
proof: Proof. Open Scope Z_scope. intros (a1,a2) (b1,b2) (c1,c2). unfold Qle, Qlt; simpl. simpl_mult. rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1). rewrite Z.mul_1_r. intro LT. rewrite <- Z.mul_lt_mono_pos_r. - reflexivity. - now apply Z.mul_pos_pos. Close Scope Z_scope. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool