proposition: Lemma BQ_P q: ratp q <-> [/\ pairp q, intp (Qnum q), inc (Qden q) BZps & BZcoprime (Qnum q) (Qden q)].
proof: Proof. split. by move /Zo_P => [/setX_P [pq Pq Qq] cp]; split. by move => [pa Pq Qq cp]; apply:Zo_i => //; apply/setX_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)