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