proposition: Lemma continuous_real f x: realp x -> continuous_at f x -> realp (f x).
proof: Proof. move => xr h1; move:(h1 _ RpsS1) => [d /BRps_sBRp de h2]. have /h2 [//]: (BR_near x d x). by split => //; rewrite BRdiff_xx // BRabs_0; apply/ rle0xP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)