proposition: Lemma sgzP x : sgz_val x (0 == x) (x <= 0) (0 <= x) (x == 0) (x < 0) (0 < x) (0 == sgr x) (-1 == sgr x) (1 == sgr x) (sgr x == 0) (sgr x == -1) (sgr x == 1) (0 == sgz x) (-1 == sgz x) (1 == sgz x) (sgz x == 0) (sgz x == -1) (sgz x == 1) `|x| (sgr x) (sgz x).
proof: Proof. rewrite ![_ == sgz _]eq_sym ![_ == sgr _]eq_sym !sgr_cp0 !sgz_cp0. by rewrite /sgz; case: sgrP; constructor. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)