proposition: Lemma lee_wpmul2r x : 0 <= x -> {homo *%E^~ x : y z / y <= z}.
proof: Proof. move: x => [x|_|//]. rewrite lee_fin le_eqVlt => /predU1P[<- y z|x0]; first by rewrite 2!mule0. move=> [y| |] [z| |]//; first by rewrite !lee_fin// ler_pM2r. - by move=> _; rewrite mulr_infty gtr0_sg// mul1e leey. - by move=> _; rewrite mulr_infty gtr0_sg// mul1e leNye. - by move=> _; rewrite 2!mulr_infty gtr0_sg// 2!mul1e. move=> [y| |] [z| |]//. - rewrite lee_fin => yz. have [z0|z0|] := ltgtP 0%R z. + by rewrite [leRHS]mulr_infty gtr0_sg// mul1e leey. + by rewrite mulr_infty ltr0_sg// ?(le_lt_trans yz)// [leRHS]mulr_infty ltr0_sg. + move=> z0; move: yz; rewrite -z0 mul0e le_eqVlt => /predU1P[->|y0]. by rewrite mul0e. by rewrite mulr_infty ltr0_sg// mulN1e leNye. + by move=> _; rewrite mulyy leey. + by move=> _; rewrite mulNyy leNye. + by move=> _; rewrite mulNyy leNye. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed