proposition: Lemma BQabs0_bis x: ratp x -> (x = \0q <-> BQabs x = \0q).
proof: Proof. move => pa; split; first by move => ->; rewrite BQabs_0. move /pr1_def => pb; apply:BQnum0_P => //. by move/BQ_P:pa =>[_ / BZabs_0p pc _ _]; apply: pc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)