proposition: Lemma BQdiv_numden1 a b (q := BQ_of_Z a /q BQ_of_Z b): intp a -> inc b BZps -> BZcoprime a b -> (Qnum q = a /\ Qden q = b).
proof: Proof. move => az bz abc. suff: q = J a b by move => ->; aw. rewrite / q /BQdiv /BQinv /BQ_of_Z pr1_pair (Y_true bz) /BQprod; aw. rewrite (BZprod_1r az) (BZprod_1l (BZps_sBZ bz)) /BQ_of_pair -lock /BQ_of_pair_internal abc. by rewrite (BZquo_one az) (BZquo_one (BZps_sBZ bz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)