proposition: Lemma continuous2_sum : continuous2 BRsum.
proof: Proof. apply:continuous2_sym; first by move => x y _ _ ;apply: BRsumC. move => x y xr yr e ep; ex_tac => z [za zb]. split; [ by apply: RSs | by rewrite BRdiff_sum_simpl_l]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)