proposition: Lemma BQ_of_pair_prop4 a b: intp a -> inc b BZps -> ratp (BQ_of_pair a b).
proof: Proof. move => az bz. have [qz qp cp _ ] := (BQ_of_pair_prop1 az bz). rewrite /BQ_of_pair -lock /BQ_of_pair_internal; set b':= (b %/z BZgcd a b). apply/BQ_P; split => //; aww. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)