proposition: Lemma lee_pdivr_mull r x y : (0 < r)%R -> (r^-1%:E * y <= x) = (y <= r%:E * x).
proof: Proof. move=> r0; apply/idP/idP. - rewrite le_eqVlt => /predU1P[<-|]; last by rewrite lte_pdivr_mull// => /ltW. by rewrite muleA -EFinM divrr ?mul1e// unitfE gt_eqF. - rewrite le_eqVlt => /predU1P[->|]; last by rewrite -lte_pdivr_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