proposition: Lemma Qint_def (x : rat) : (x \is a Num.int) = (denq x == 1).
proof: Proof. by []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)