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