proposition: Lemma neq0_mulr_lt0 x y : x != 0 -> y != 0 -> (x * y < 0) = (x < 0) (+) (y < 0).
proof: Proof. by move=> x_neq0 y_neq0; rewrite mulr_lt0 x_neq0 y_neq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)