proposition: Lemma lee_pdivl_mull r y x : (0 < r)%R -> (x <= r^-1%:E * y) = (r%:E * x <= y).
proof: Proof. move=> r0; apply/idP/idP. - rewrite le_eqVlt => /predU1P[->|]; last by rewrite lte_pdivl_mull// => /ltW. by rewrite muleA -EFinM divrr ?mul1e// unitfE gt_eqF. - rewrite le_eqVlt => /predU1P[<-|]; last by rewrite -lte_pdivl_mull// => /ltW. by rewrite muleA -EFinM mulVr ?mul1e// unitfE gt_eqF. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed