proposition: Lemma qle_abs x: ratp x -> x <=q (BQabs x).
proof: Proof. move => xq;case /BQ_i0P: (xq) => xp. move: (QpSa xq) => / qle0xP pa; move / qgt0xP: xp => [pb _]; BQo_tac. by rewrite (BQabs_pos xp); apply:qleR. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)