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