proposition: Lemma BQprod_inv1 x : ratp x -> x <> \0q -> (x *q (BQinv x)) = \1q.
proof: Proof. wlog xp:x /(inc x BQps). move => H xq xns; case /BQ_i1P:xq => xs //. by apply:(H _ xs (BQps_sBQ xs) xns). move: (BQopp_negative1 xs) => oxp. move:(BQms_sBQ xs) => xq; move:(QSo xq)=> oxq. rewrite -( BQprod_opp_opp xq (QS_inv xq)) - (BQinv_opp xq); apply: H => //. by move /BQps_iP:oxp => [_ ]. move => _ _ ;rewrite (BQinv_pos xp) /BQprod; aw. move/Zo_P: xp => [/BQ_P [_ sa sb _] sc]. move: (ZpsS_prod sb sc)=> /BZps_iP [hb hd]; move:(BZp_sBZ hb) => hc. rewrite BZprodC /BQ_of_pair -lock /BQ_of_pair_internal (BZgcd_id hc) (BZabs_pos hb). by rewrite(proj2(BZdvd_itself hc hd)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)