proposition: Lemma BRdouble_half1 x: realp x -> BRhalf x +r BRhalf x = x.
proof: Proof. move => h. by rewrite /BRhalf - (BRprodDr h RSh2 RSh2) BRdouble_half2 BRprod_1r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)