proposition: Lemma numq_eq0 x : (numq x == 0) = (x == 0).
proof: Proof. rewrite -[x]valqK fracq_eq0; case: fracqP=> /= [|k {}x k0]. by rewrite eqxx orbT. by rewrite !mulf_eq0 (negPf k0) /= denq_eq0 orbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)