proposition: Lemma BRdiff_diff 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; rewrite /BRdiff. by rewrite (BRoppD br (RSo cr)) (BRopp_K cr) BRsumA //; apply:RSo. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)