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