proposition: Lemma BQprod_m1r x: ratp x -> x *q \1mq = BQopp x.
proof: Proof. move => xq; rewrite /BQprod /BQ_of_pair /BQ_mone /BQ_of_Z; aw. move /BQ_P: (xq) => [_ pa /BZps_sBZ pc _]. move: (BQ_pr2 (QSo xq)); rewrite /BQopp; aw. rewrite BZprod_1r // BZprod_m1r //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)