proposition: Lemma Qmult_le_r (x y z: Q): 0 < z -> (x*z <= y*z <-> x <= y).
proof: Proof. split; intro. - now apply Qmult_lt_0_le_reg_r with z. - apply Qmult_le_compat_r; auto with qarith. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool