proposition: Lemma BRcompare_zero x: inc x BRps -> exists2 y, inc y BQps & BR_of_Q y <r x.
proof: Proof. move => h. move:(setC_ne (BR_hi_Qps' h)) => [y /setC_P [ya yb]]. have h':=(BR_le_aux3 (BRps_sBR h) (BQps_sBQ ya) yb). case: (equal_or_not (BR_of_Q y) x) => eq; last by ex_tac. move:(BQhalf_pos ya)(BQhalf_pos1 ya) => sa sb; ex_tac. by move/(rlt_cQ (proj31_1 sb) (proj32_1 sb)): sb; rewrite eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)