proposition: Lemma BR_le_aux3 x a: realp x -> ratp a -> ~(inc a x) -> (BR_of_Q a) <=r x.
proof: Proof. move => xr aq h. have pf:=(RS_of_Q aq). split => // t tx; move:(BRi_sQ xr tx) => tq;apply: (Zo_i tq). case: (qleT_ell aq tq) => //. by move => eat;case:h; rewrite eat. move => ta; case: h;exact:(BRi_segment xr tx ta). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)