proposition: Lemma ratP x : rat_spec x (numq x) (denq x).
proof: Proof. rewrite -{1}[x](divq_num_den); case hd: denq => [p|n]. have: 0 < p%:Z by rewrite -hd denq_gt0. case: p hd=> //= n hd; constructor; rewrite -?hd ?divq_num_den //. by rewrite -[n.+1]/`|n.+1|%N -hd coprime_num_den. by move: (denq_gt0 x); rewrite hd. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)