proposition: Lemma BQopp0_bis x: ratp x -> (x = \0q <-> BQopp x = \0q).
proof: Proof. move => xq; split => h; first by rewrite h; exact BQopp_0. apply:(BQnum0_P xq); move/BQ_P:xq => [_ nz _ _]. by rewrite -(BZopp_K nz) (pr1_def h) BZopp_0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)