fact: Definition Cauchy_fun_seq1 := forall k, {N : nat | forall m n, N <= m -> N <= n -> Norm_Funct (Continuous_I_minus _ _ _ _ _ (contf m) (contf n)) [<=] one_div_succ k}.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval