proposition: Lemma BRmiddle_comp x y: x <r y -> x <r BRmiddle x y /\ BRmiddle x y <r y.
proof: Proof. move => cp. move: (cp) => [[xr yr _] _]. split. have : x *r \2r <r x +r y. by rewrite - (BRdouble_s xr); apply /(BRsum_lt2l xr yr xr). move /(BRprod_plt2r (RSp xr RS2) (RSs xr yr) RpsSh2). by rewrite -/(BRhalf (x *r \2r)) (BRhalf_double xr). have : x +r y <r y *r \2r. by rewrite - (BRdouble_s yr); apply /(BRsum_lt2r xr yr yr). move /(BRprod_plt2r (RSs xr yr) (RSp yr RS2) RpsSh2). by rewrite -/(BRhalf (y *r \2r)) (BRhalf_double yr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)