proposition: Lemma coprimeq_num n d : coprime `|n| `|d| -> numq (n%:~R / d%:~R) = sgr d * n.
proof: Proof. move=> cnd /=; have <- := fracqE (n, d). rewrite num_fracq/= (eqP (cnd : _ == 1)) divn1. have [|d_gt0|d_lt0] := sgrP d; by rewrite (mul0r, mul1r, mulN1r) //= ?[_ ^ _]signrN ?mulNr mulz_sign_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)