proposition: Lemma continuous_local f g x: realp x -> (exists2 e, inc e BRps & forall y, BR_near x e y -> f y = g y) -> continuous_at f x -> continuous_at g x.
proof: Proof. move => xr [e ep ev] cfx. move => e1 e1p. move:(cfx e1 e1p) => [d dp dv]. move:(rmin_prop2 ep dp) (rmin_prop1 (BRps_sBR ep) (BRps_sBR dp)). set e2:= (rmin e d); move => sa [sb sc sd]; ex_tac => y ya. move:(dv _ (BR_near_trans sd ya)). rewrite (ev _ (BR_near_trans sc ya)). have hh: BR_near x e2 x. split => //;rewrite (BRdiff_xx xr) BRabs_0; apply/ rle0xP => //. exact:(BRps_sBRp sa). by rewrite (ev _ (BR_near_trans sc hh)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)