proposition: Lemma sgrMn x n : sg (x *+ n) = (n != 0)%:R * sg x.
proof: Proof. case: n => [|n]; first by rewrite mulr0n sgr0 mul0r. by rewrite !sgr_def mulrn_eq0 mul1r pmulrn_llt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)