proposition: Lemma BRdiff_diff2 a b c: realp a -> realp b -> realp c -> (a -r b) -r c = a -r (b +r c).
proof: Proof. move => ar br cr. by rewrite /BRdiff - (BRsumA ar (RSo br) (RSo cr)) BRoppD. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)