proposition: Lemma BR_le_aux2 x a: realp x -> inc a x -> x <r (BR_of_Q a).
proof: Proof. move => xr ax. have pf:=(RS_of_Q (BRi_sQ xr ax)). split; last by move => eq; move: ax; rewrite eq => /Zo_hi [_]. by split => // t /Zo_P [_ tx]; apply: (BRi_segment xr ax tx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)