proposition: Lemma lee_pmul2l x : x \is a fin_num -> 0 < x -> {mono *%E x : x y / x <= y}.
proof: Proof. move: x => [x _|//|//] /[!(@lte_fin R)] x0 [y| |] [z| |]. - by rewrite -2!EFinM 2!lee_fin ler_pM2l. - by rewrite mulry gtr0_sg// mul1e 2!leey. - by rewrite mulrNy gtr0_sg// mul1e 2!leeNy_eq. - by rewrite mulry gtr0_sg// mul1e 2!leye_eq. - by rewrite mulry gtr0_sg// mul1e. - by rewrite mulry mulrNy gtr0_sg// mul1e mul1e. - by rewrite mulrNy gtr0_sg// mul1e 2!leNye. - by rewrite mulrNy mulry gtr0_sg// 2!mul1e. - by rewrite mulrNy gtr0_sg// mul1e. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed