proposition: Lemma Qmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> 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_le_mono_nonneg_r; auto. now apply Z.mul_nonneg_nonneg. Close Scope Z_scope. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool