proposition: Lemma BQdiv_numden x: ratp x -> (BQ_of_Z (Qnum x)) /q (BQ_of_Z (Qden x)) = x.
proof: Proof. wlog xp: x/ inc x BQps. move => H; case /BQ_i1P => xs. + rewrite xs BQnum0 BQden0 -/BQ_zero -/BQ_one /BQdiv BQprod_0l ?BQinv_1 //. apply: QS1. + by apply: H => //; apply: BQps_sBQ. + move:(BQopp_negative1 xs) => h; move: (BQps_sBQ h) => h1. move: (BQms_sBQ xs) => xq. move/BQ_P: (xq) => [_ pa /BZps_sBZ pb _]; move:(ZSo pa) => pc. move: (H _ h h1); rewrite {1 2} /BQopp; aw => sa. move: (f_equal BQopp sa); rewrite (BQopp_K xq) => {3} <-. rewrite BQopp_div_l; try apply /BQ_of_Z_iQ => //;congr (_ /q _). by rewrite /BQ_of_Z /BQopp pr1_pair BZopp_K //; aw. move => xq; move/BQ_P: (xq) => [_ pb pc _]. have pf := BZps_sBZ pc. rewrite /BQdiv (BQinv_pos (BQ_of_Z_iQps pc)) /BQ_of_Z /BQprod; aw. by rewrite BZprod_1r // BZprod_1l // BQ_pr2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)