proposition: Lemma denqN x : denq (- x) = denq x.
proof: Proof. rewrite [- _]oppq_def den_fracq. case: x => -[a b]; rewrite /denq/= => /andP[b_gt0]. by rewrite /coprime=> /eqP cab; rewrite gt_eqF // abszN cab divn1 gtz0_abs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)