proposition: Lemma BRcompare_zero' e: inc e BQps -> exists2 e', inc e' BRps & e' <r (BR_of_Q e).
proof: Proof. move => ep. move:(BQhalf_pos1 ep)(BQhalf_pos ep). set e1 := BQhalf e => sa sb. move /(rlt_cQ (proj31_1 sa) (proj32_1 sa)): sa => sa'. move: (RpsS_of_Q sb) => sc; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)