proposition: Lemma continuous_prop2 f x a: continuous_at f x -> f x <r a -> exists2 e, inc e BRps & forall y, (BR_near x e y) -> f y <r a.
proof: Proof. move => ha lt1. have fr: realp (f x) by BRo_tac. pose g x := BRopp (f x). have ra:= (continuous_comp ha (continuous_opp fr)). move:(continuous_prop1 ra (rlt_opp lt1)) => [e ep h]. move:(ha _ ep) => [d dp dq]. move:(rmin_prop2 dp ep) => mp. move:(rmin_prop1 (BRps_sBR dp) (BRps_sBR ep)) => [_ sa sb]. ex_tac => y yn; move:(dq _ (BR_near_trans sa yn)) =>[fyr _]. by move:(h _ (BR_near_trans sb yn)) =>/(rlt_oppP fyr (proj32_1 lt1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)