proposition: Lemma fun_Cauchy_prop_const : forall H (contH:Continuous_I Hab H), Cauchy_fun_seq a b Hab (fun n => H) (fun n => contH).
proof: Proof. intros. apply conv_Cauchy_fun_seq' with H contH. apply fun_Lim_seq_const. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval