proposition: Lemma rle_cQ x y: ratp x -> ratp y -> (x <=q y <-> (BR_of_Q x <=r BR_of_Q y)).
proof: Proof. move => xsq ysq;split => [lxy | [_ _ se]]. split; [ by apply: RS_of_Q | by apply: RS_of_Q | ]. move => t /Zo_P [ta tb]; apply/Zo_P; split => //; BQo_tac. case: (qleT_el xsq ysq) => // cxy. have: inc x (BR_of_Q y) by apply:Zo_i => //; split => //; apply:nesym. by move/se => /Zo_hi [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)