proposition: Lemma BRoppD x y: realp x -> realp y -> BRopp (x +r y) = (BRopp x) +r (BRopp y).
proof: Proof. move => xr yr. move: (RSo xr)(RSo yr) => oxr oyr. symmetry; apply: BRsum_opp_rev; try apply:RSs => //. rewrite BRsum_ACA // (BRsumC _ y) (BRsum_opp_r yr). by rewrite (BRsumC _ x) (BRsum_opp_r xr)(BRsum_0l RS0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)