proposition: Lemma BRsum_opp_rev a b: realp a -> realp b -> a +r b = \0r -> a = BRopp b.
proof: Proof. move => ar br h. move: (BRsumA ar br (RSo br)). by rewrite (BRsum_opp_r br) h (BRsum_0l (RSo br)) (BRsum_0r ar). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)