proposition: Lemma BR_of_Q_inj1: {inc BQ &, injective BR_of_Q}.
proof: Proof. move => u v uq vq eq. case: (qleT_ell uq vq) => lt. + exact. + have: inc v (BR_of_Q u) by apply:Zo_i. by rewrite eq=> /Zo_hi [_]. + have: inc u (BR_of_Q v) by apply:Zo_i. by rewrite - eq=> /Zo_hi [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)