proposition: Lemma BQinv_opp x: ratp x -> BQinv (BQopp x) = BQopp (BQinv x).
proof: Proof. move => xq; move/BQ_P: (xq) => [_ nz dzp _]; move:(BZps_sBZ dzp)=> dz. case /BQ_i1P: xq => xs. + by rewrite xs BQopp_0 BQinv_0 BQopp_0. + have h := (BQopp_positive1 xs). by rewrite (BQinv_pos xs) (BQinv_neg h) /BQopp !pr1_pair BZopp_K;aw. + have h := (BQopp_negative1 xs). by rewrite (BQinv_pos h) (BQinv_neg xs) /BQopp; aw; rewrite BZopp_K. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)