proposition: Lemma BR_nearP x e y: realp x -> realp e -> ((BR_near x e y) <-> ( x -r e <=r y /\ y <=r x +r e)).
proof: Proof. move => xr er; case: (inc_or_not y BR)=> yr; last first. split; [ by move => [] | by move => [/proj32 H]]. have ha:=(BRdiff_le1P xr er yr). have hb: BRopp e <=r x -r y <-> y <=r x +r e. by move:(BRdiff_le2P xr yr (RSo er)); rewrite /BRdiff (BRopp_K er). split; move=> [sa sb]. move/(BRabs_prop1 (RS_diff xr yr) er): sb => [su sv]. split; [ by apply/ha | by apply/hb]. split => //; apply/(BRabs_prop1 (RS_diff xr yr) er). split; [ by apply/hb | by apply/ha]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)