proposition: Lemma Rdiv_le_mult : forall x y z, y > 0 -> x / y <= z <-> x <= y * z.
proof: Proof. intros. split; intro. - eapply Rmult_le_reg_r. + apply Rinv_0_lt_compat. exact H. + replace (y * z * /y) with z; trivial. rewrite Rmult_comm, <- Rmult_assoc, Rinv_l; lra. - unfold Rdiv. eapply Rmult_le_reg_r. + eassumption. + rewrite Rmult_assoc, Rinv_l, Rmult_1_r; lra. Qed.
imports: Coq(Reals.Ratan Lia Lra Logic.IndefiniteDescription Program.Subset) ZornsLemma(Quotients) Topology(ProductTopology AdjunctionSpace SubspaceTopology RTopology RFuncContinuity Homeomorphisms)