proposition: Lemma BR_le_aux1 x a: realp x -> (exists2 b, inc b x & b <q a) -> x <r (BR_of_Q a).
proof: Proof. move => xr [b bx lba]; move:(RS_of_Q (proj32_1 lba)) => sa. case: (inc_or_not b (BR_of_Q a)); first by move => /Zo_P [_] [h _]; BQo_tac. move => bna;split; last by move => eq; case: bna; rewrite - eq. split => // t /Zo_P [ta tb]; apply:(BRi_segment xr bx); BQo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)