proposition: Lemma BQ_pr2 q: ratp q -> BQ_of_pair (Qnum q) (Qden q) = q.
proof: Proof. move /BQ_P => [pq nz /BZps_sBZ dz cp]. by rewrite /BQ_of_pair -lock /BQ_of_pair_internal cp (BZquo_one nz) (BZquo_one dz) pq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)