proposition: Lemma lee_pmul2r x : x \is a fin_num -> 0 < x -> {mono *%E^~ x : x y / x <= y}.
proof: Proof. by move=> xfin x0 y z; rewrite -2!(muleC x) lee_pmul2l. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed