proposition: Lemma Qle_div_l : forall a b c, 0 < b -> 0 < c -> (a / b <= c <-> a / c <= b).
proof: Proof. intros a b c A1 A2. rewrite <- Qle_shift_div_r; [| easy]. rewrite (Qmult_comm c b). rewrite Qle_shift_div_r; easy. 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