proposition: Lemma mulr_sign_lt0 (b : bool) x : ((-1) ^+ b * x < 0) = (x != 0) && (b (+) (x < 0)%R).
proof: Proof. by rewrite mulr_lt0 signr_lt0 signr_eq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)