proposition: Lemma mule_eq_pinfty x y : (x * y == +oo) = [|| (x > 0) && (y == +oo), (x < 0) && (y == -oo), (x == +oo) && (y > 0) | (x == -oo) && (y < 0)].
proof: Proof. move: x y => [x| |] [y| |]; rewrite ?(lte_fin,andbF,andbT,orbF,eqxx,andbT)//=. - by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP x 0%R; move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e). - by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP x 0%R; move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e). - by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP y 0%R; move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e). - by rewrite mulyy ltry. - by rewrite mulyNy. - by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP y 0%R; move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e). - by rewrite mulNyy. - by rewrite ltNyr. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed