proposition: Lemma leR_pdivl_mulr z x y : 0 < z -> (x <= y / z) <-> (x * z <= y).
proof: Proof. move=> z0; split => [/(leR_wpmul2l (ltRW z0))|H]. - rewrite mulRC mulRCA mulRV ?mulR1 //; exact/gtR_eqF. - apply/(@leR_pmul2r z) => //; rewrite -mulRA mulVR ?mulR1 //; exact/gtR_eqF. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)