proposition: Lemma sgrMz m x : sgr (x *~ m) = sgr x *~ sgr m.
proof: Proof. by rewrite -mulrzr sgrM -intr_sg mulrzr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)