proposition: Fact scalq_eq0 x : (scalq x == 0) = (x.2 == 0).
proof: Proof. case: x => n d; rewrite scalq_def /= mulf_eq0 sgr_eq0 /= eqz_nat. rewrite -[gcdn _ _ == 0]negbK -lt0n gcdn_gt0 ?absz_gt0 [X in ~~ X]orbC. by case: sgrP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)