proposition: Lemma BR_le_aux4 x: realp x -> (inc \0q x <-> x <r \0r).
proof: Proof. move => xr; split => h; first by apply:(BR_le_aux2 xr h). ex_middle bad; move:(BR_le_aux3 xr QS0 bad) => h'; BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)