proposition: Lemma mule_eq_ninfty x y : (x * y == -oo) = [|| (x > 0) && (y == -oo), (x < 0) && (y == +oo), (x == -oo) && (y > 0) | (x == +oo) && (y < 0)].
proof: Proof. have := mule_eq_pinfty x (- y); rewrite muleN eqe_oppLR => ->. by rewrite !eqe_oppLR lteNr lteNl oppe0 (orbC _ ((x == -oo) && _)). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed