proposition: Lemma BR_pos_prop x: inc x BRps <-> (realp x /\ exists2 y, inc y BQps & ~ inc y x).
proof: Proof. apply: (iff_trans (iff_sym (rlt0xP x))); split. move => [[_ pb pc] pd]; split => //. move:(setC_ne (conj pc (nesym pd))) => [y /setC_P [ /Zo_hi/ qlt0xP pa] pe]. ex_tac. move => [pa [y / qlt0xP yb yc]]. case: (rleT_ell RS0 pa) => // h; case: yc. rewrite - h; apply: Zo_i => //. rewrite -/(ratp _);BQo_tac. move/(BR_le_aux4 pa):h => xp; apply: (BRi_segment pa xp yb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)