proposition: Lemma rlt_cQ x y: ratp x -> ratp y -> (x <q y <-> (BR_of_Q x <r BR_of_Q y)).
proof: Proof. move => xq yq;split; move => [lxy nexy]; split. + by apply/(rle_cQ xq yq). + move => eq. have: inc y (BR_of_Q x) by apply:Zo_i. by rewrite eq; move /Zo_hi => [_]. + by apply/(rle_cQ xq yq). + by dneg xy; rewrite xy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)