proposition: Lemma sgzM x y : sgz (x * y) = sgz x * sgz y.
proof: Proof. rewrite -sgz_sgr -(sgz_sgr x) -(sgz_sgr y) sgrM. by case: sgrP; case: sgrP; rewrite /sgz ?(mulNr, mul0r, mul1r); rewrite ?(oppr_eq0, oppr_cp0, eqxx, ltxx, ltr01, ltr10, oner_eq0). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)