proposition: Lemma pmulR_lgt0' [x y : R] : 0 < y * x -> 0 <= x -> 0 < y.
proof: Proof. case/boolP: (x == 0) => [/eqP -> |]; first by rewrite mulR0 => /ltRR. move=> /eqP /nesym ? /[swap] ? /pmulR_lgt0; apply. by rewrite ltR_neqAle; split. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)