proposition: Lemma intr_sg m : (sgr m)%:~R = sgr (m%:~R) :> R.
proof: Proof. by rewrite sgrz -sgz_int -sgrEz. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)