proposition: Lemma BR_middle_prop2 a b: realp a -> realp b -> (BRmiddle a b) -r a = BRhalf (b -r a).
proof: Proof. move => ar br. rewrite /BRmiddle -{2} (BRhalf_double ar) /BQhalf. rewrite - (BRprodBl RSh2 (RSs ar br)(RSp ar RS2)) - (BRdouble_s ar). by rewrite BRdiff_sum_simpl_l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)