proposition: Lemma leR_pmul2l x y z : x > 0 -> (x * y <= x * z <-> y <= z).
proof: Proof. move=> x_gt0; have invx_gt0: x^-1 > 0 by apply: invR_gt0. by split=> [/(leMl invx_gt0) | /(leMl x_gt0)//]; rewrite !pmulKR. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)