proposition: Lemma denqVz (i : int) : i != 0 -> denq (i%:~R^-1) = `|i|.
proof: Proof. move=> h; rewrite -div1r -[1]/(1%:~R). by rewrite coprimeq_den /= ?coprime1n // (negPf h). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)