proposition: Lemma coprimeq_den n d : coprime `|n| `|d| -> denq (n%:~R / d%:~R) = (if d == 0 then 1 else `|d|).
proof: Proof. move=> cnd; have <- := fracqE (n, d). by rewrite den_fracq/= (eqP (cnd : _ == 1)) divn1; case: d {cnd}; case. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)