proposition: Lemma continuous_sum f g x: realp x -> continuous_at f x -> continuous_at g x -> continuous_at (fun z => f z +r g z) x.
proof: Proof. move => xr pa pb. move => e ep; move: (BRhalf_pos ep) => hep. move:(pa _ hep)(pb _ hep) =>[d1 d1ps d1v] [d2 d2ps d2v]. move:(rmin_prop2 d1ps d2ps) (rmin_prop1 (BRps_sBR d1ps) (BRps_sBR d2ps)). set d3:= (rmin d1 d2); move => sa [sb sc sd]; ex_tac => y [yr ya]. have ha: BR_near x d1 y by split => //; BRo_tac. have hb: BR_near x d2 y by split => //; BRo_tac. move:(d1v _ ha) (d2v _ hb) => [ua ub] [uc ud]. move:(continuous_real xr pa)(continuous_real xr pb) => fxr gxr. split; first by apply: RSs. rewrite /BRdiff (BRoppD ua uc). rewrite (BRsum_ACA fxr gxr (RSo ua) (RSo uc)). move:(rle_triangular (RS_diff fxr ua) (RS_diff gxr uc)). move:(BRsum_Mlele ub ud); rewrite (BRdouble_half1 (BRps_sBR ep)). move => h1 h2; BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)