proposition: Lemma lte_pdivr_mull r x y : (0 < r)%R -> (r^-1%:E * y < x) = (y < r%:E * x).
proof: Proof. move=> r0; move: x y => [x| |] [y| |] //=. - by rewrite 2!lte_fin ltr_pdivrMl. - by rewrite mulr_infty sgrV gtr0_sg// mul1e 2!ltNge 2!leey. - by rewrite mulr_infty sgrV gtr0_sg// mul1e -EFinM 2!ltNyr. - by rewrite mulr_infty gtr0_sg// mul1e 2!ltry. - by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e ltxx. - by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// 2!mul1e. - by rewrite mulr_infty gtr0_sg// mul1e. - by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// 2!mul1e. - by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed