proposition: Lemma BQabs_positive b: ratp b -> b <> \0q -> \0q <q (BQabs b).
proof: Proof. move => pa pb; apply /qlt0xP. by apply /BQps_iP;split; [ apply:QpSa | move/(BQabs0_bis pa) ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)