proposition: Lemma sgz_eq (R R' : realDomainType) (x : R) (y : R') : (sgz x == sgz y) = ((x == 0) == (y == 0)) && ((0 < x) == (0 < y)).
proof: Proof. by do 2!case: sgzP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)