proposition: Lemma BR_hi_Qps x: inc x BRp -> sub x BQps.
proof: Proof. move => /Zo_P [h1 h2] t tx. apply/BQps_iP; split; [by apply: h2 | move => t0; rewrite t0 in tx]. move/BR_P: h1 => [_ _ _ _ h3]; move:(h3 _ tx) => [y yx / qgt0xP y0]. exact:(BQ_di_neg_pos y0 (h2 _ yx)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)