proposition: Fact fracq_eq0 x : (fracq x == zeroq) = (x.1 == 0) || (x.2 == 0).
proof: Proof. move: x=> [n d] /=; have [->|d0] := eqVneq d 0. by rewrite fracq0 eqxx orbT. by rewrite -[zeroq]valqK orbF fracq_eq ?d0 //= mulr1 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)