fact: Definition sgz x : int := if x == 0 then 0 else if x < 0 then -1 else 1.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)