proposition: Lemma Qle_shift_div_r : forall a b c, 0 < b -> (a <= c * b <-> a / b <= c).
proof: Proof. intros a b c A; split; [now apply Qle_shift_div_r |]. intro A1. apply (Qmult_le_r _ _ (/b)); [now apply Qinv_lt_0_compat |]. rewrite <- Qmult_assoc, Qmult_inv_r; [now rewrite Qmult_1_r | auto with qarith]. 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