proposition: Lemma conv_fun_seq'_norm : conv_fun_seq' -> conv_norm_fun_seq.
proof: Proof. intro H. red in |- *; red in H. intro. elim (H (one_div_succ k) (one_div_succ_pos _ k)). intros N HN. exists N. intros. apply leEq_Norm_Funct. fold I in |- *; intros x H1 Hx. eapply leEq_wdl. apply (HN n H0 x H1). apply AbsIR_wd; simpl in |- *; rational. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval