proposition: Lemma sgr_lt0 x : (sg x < 0) = (x < 0).
proof: Proof. rewrite /sg; case: eqP => [-> // | _]. by case: ifP => _; rewrite ?ltrN10 // lt_gtF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)