proposition: Lemma coprime_num_den x : coprime `|numq x| `|denq x|.
proof: Proof. by rewrite /numq /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)