proposition: Lemma mulr_lt0 x y : (x * y < 0) = [&& x != 0, y != 0 & (x < 0) (+) (y < 0)].
proof: Proof. have [x_gt0|x_lt0|->] /= := ltrgt0P x; last by rewrite mul0r. by rewrite pmulr_rlt0 //; case: ltrgt0P. by rewrite nmulr_rlt0 //; case: ltrgt0P. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)