proposition: Lemma continuous2_diff : continuous2 BRdiff.
proof: Proof. move => x y xr yr;move:(continuous2_sum xr (RSo yr)) => [sa sb]. split => //; apply:(continuous_comp (continuous_opp yr) sa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)