fact: Definition Rbar_locally (a : Rbar) (P : R -> Prop) := match a with | Finite a => locally a P | p_infty => exists M : R, forall x, M < x -> P x | m_infty => exists M : R, forall x, x < M -> P x end.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub