proposition: Lemma sgr_scalq x : sgr (scalq x) = sgr x.2.
proof: Proof. rewrite scalq_def sgrM sgr_id -[(gcdn _ _)%:Z]intz sgr_nat. by rewrite -lt0n gcdn_gt0 ?absz_gt0 orbC; case: sgrP; rewrite // mul0r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)