fact: Definition Cauchy_fun_seq := forall e, [0] [<] e -> {N : nat | forall m n, N <= m -> N <= n -> forall x Hx, AbsIR (f m x (incf m x Hx) [-]f n x (incf n x Hx)) [<=] e}.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval