proposition: Lemma mulr_sg_eqN1 x y : (sg x * sg y == -1) = (x != 0) && (sg x == - sg y).
proof: Proof. move/sg: y => y; rewrite /sg eq_sym eqr_oppLR. case: ifP => _; first by rewrite mul0r oppr0 oner_eq0. by case: ifP => _; rewrite ?mul1r // mulN1r eqr_oppLR. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)