proposition: Lemma ltR_pdivl_mulr z x y : 0 < z -> (x < y / z) <-> (x * z < y).
proof: Proof. move=> z0; split => [/(ltR_pmul2l z0)|H]. - by rewrite mulRC mulRCA mulRV ?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)