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