proposition: Lemma QSo x: ratp x -> ratp (BQopp x).
proof: Proof. rewrite /BQopp => xq; move/BQ_P: xq => [_ nz dn cp]; apply /BQ_P; aw. have pc':= (BZps_sBZ dn). by split; [ fprops | apply:ZSo | exact| rewrite /BZcoprime - BZgcd_opp ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)