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