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