proposition: Lemma continuous_prop1 f x a: continuous_at f x -> a <r f x -> exists2 e, inc e BRps & forall y, (BR_near x e y) -> a <r f y.
proof: Proof. move => ha hb. move:(hb) =>[[ar fxr _] _ ]. have ep: inc (f x -r a) BRps by apply/ rlt0xP; apply/(rlt_diffP1 ar fxr). have hep:=(BRhalf_pos ep). have her:=(BRps_sBR hep). move:(ha _ hep) => [d dp dv]; ex_tac => y /dv [ya yb]. move/ rlt0xP: hep => hep. move/ (BRabs_prop3 fxr ya her): yb => [ _ la]. move:(BRsum_Mlegt0 la hep). rewrite - (BRsumA ya her her) (BRdouble_half1 (BRps_sBR ep)) /BRdiff. rewrite (BRsumC (f x)) (BRsumA ya (RSo ar) fxr) => hc. move/(rlt_diffP1 fxr (proj32_1 hc)) : hc. by rewrite( BRdiff_sum1 fxr (RS_diff ya ar)) => /(rlt_diffP1 ar ya). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)