proposition: Lemma lte_pdivl_mull r y x : (0 < r)%R -> (x < r^-1%:E * y) = (r%:E * x < y).
proof: Proof. move=> r0; move: x y => [x| |] [y| |] //=. - by rewrite 2!lte_fin ltr_pdivlMl. - by rewrite mulr_infty sgrV gtr0_sg// mul1e 2!ltry. - by rewrite mulr_infty sgrV gtr0_sg// mul1e. - by rewrite mulr_infty gtr0_sg// mul1e. - by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e. - by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// 2!mul1e. - by rewrite mulr_infty gtr0_sg// mul1e 2!ltNyr. - 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