proposition: Lemma QpSa x: ratp x -> inc (BQabs x) BQp.
proof: Proof. move => xq. case/BQ_i0P: (xq) => h; last by rewrite (BQabs_pos h). rewrite (BQabs_negs h); apply: (BQopp_negative2 (BQms_sBQm h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)