proposition: Lemma sgrP x : sgr_val x `|x| (0 == x) (x <= 0) (0 <= x) (x == 0) (x < 0) (0 < x) (0 == sg x) (-1 == sg x) (1 == sg x) (sg x == 0) (sg x == -1) (sg x == 1) (sg x).
proof: Proof. by rewrite ![_ == sg _]eq_sym !sgr_cp0 /sg; case: ltrgt0P; constructor. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)