proposition: Lemma conv_norm_fun_seq_wd : conv_norm_fun_seq _ _ _ _ _ contf contF -> conv_norm_fun_seq _ _ _ _ _ contf0 contF0.
proof: Proof. intros H k. elim (H k); intros N HN. exists N; intros. eapply leEq_wdl. apply (HN n H0). apply Norm_Funct_wd. apply Feq_reflexive; Included. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval