proposition: Lemma denq_gt0 x : 0 < denq x.
proof: Proof. by rewrite /denq; case: x=> [[a b] /= /andP []]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)