proposition: Lemma gt0_mulNye x : (0 < x -> -oo * x = -oo)%E.
proof: Proof. move: x => [x|_|//]; last by rewrite mulNyy. by rewrite lte_fin => x0; rewrite muleC mulr_infty gtr0_sg// mul1e. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed