proposition: Lemma sgr_numq_div (n d : int) : sgr (numq (n%:Q / d%:Q)) = sgr n * sgr d.
proof: Proof. set x := (n, d); rewrite -[n]/x.1 -[d]/x.2 -fracqE. case: fracqP => [|k fx k_neq0] /=; first by rewrite mulr0. by rewrite !sgrM mulrACA -expr2 sqr_sg k_neq0 sgr_denq mulr1 mul1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)