proposition: Lemma Qdiv_le_1 (x y: Q): 0 <= x <= y -> x / y <= 1.
proof: Proof. Proof with intuition. intros. assert (0 <= y) as ynnP by (apply Qle_trans with x; intuition). destruct y. destruct Qnum. change (x * 0 <= 1). rewrite Qmult_0_r... rewrite <- (Qmult_inv_r (Zpos p # Qden)). unfold Qdiv. apply Qmult_le_compat_r... discriminate. exfalso. apply ynnP... Qed.
imports: Coq.QArith.QArith Coq.ZArith.ZArith Coq.NArith.NArith Coq.QArith.Qpower Coq.QArith.Qround Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.List