fact: Definition fracq_opt_subdef (x : int * int) := if (0 < x.2) && coprime `|x.1| `|x.2| then x else fracq_subdef x.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)