fact: Definition extension f fi := forall (xi : I.type) (x : R), contains (I.convert xi) (Xreal x) -> contains (I.convert (fi xi)) (Xreal (f x)).
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic