proposition: Lemma continuous_opp : continuous BRopp.
proof: Proof. move => x xr e ep; ex_tac => y [yr]. rewrite (BRabs_diff xr yr)- {1} (BRopp_K yr) /BRdiff BRsumC => h; split => //. by apply: RSo. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)