proposition: Lemma real_mulrNy r : r \is Num.real -> r%:E * -oo = (Num.sg r)%:E * -oo.
proof: Proof. move=> rreal; rewrite /mule/= !eqe sgr_eq0; case: ifP => [//|rn0]. move: rreal => /orP[|]; rewrite le_eqVlt. by rewrite eq_sym rn0/= => rgt0; rewrite lte_fin rgt0 gtr0_sg// lte01. by rewrite rn0/= => rlt0; rewrite lt_def lt_geF// andbF ltr0_sg// lte0N1. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed