proposition: Lemma BRabs_prop3 x y e: realp x -> realp y -> realp e -> (BRabs (x -r y) <=r e <-> y -r e <=r x /\ x <=r y +r e).
proof: Proof. move => xr yr er. have Ha: BRopp e <=r x -r y <-> y -r e <=r x. rewrite - (BRoppB yr xr). exact (iff_trans (rle_oppP (RS_diff yr xr) er) (BRdiff_le1P yr xr er)). have Hb: x -r y <=r e <-> x <=r y +r e. move:(BRsum_le2r xr (RSs yr er) (RSo yr)). by rewrite -/(_ -r _) -/(_ -r _) (BRdiff_sum yr er). move:(BRabs_prop1 (RS_diff xr yr) er) => H. split; first by move/H => [/Ha ha /Hb hb]. by move => [/Ha ha /Hb hb]; apply/H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)