proposition: Lemma conv_fun_norm_seq : conv_norm_fun_seq -> conv_fun_seq'.
proof: Proof. intro H. red in |- *; red in H. intros e He. elim (Archimedes ([1][/] _[//]pos_ap_zero _ _ He)). intros k Hk. elim (H k); clear H. intros N HN. exists N. intros. cut (Dom (f n{-}F) x). intro H0. apply leEq_wdl with (AbsIR ((f n{-}F) x H0)). eapply leEq_transitive. 2: apply leEq_transitive with (one_div_succ (R:=IR) k). 2: apply HN with (n := n); assumption. apply norm_bnd_AbsIR; assumption. unfold one_div_succ in |- *. unfold Snring in |- *. apply less_leEq; apply swap_div with (pos_ap_zero _ _ He). apply pos_nring_S. assumption. eapply leEq_less_trans. apply Hk. simpl in |- *; apply less_plusOne. apply AbsIR_wd; simpl in |- *; rational. split. apply incf; assumption. apply incF; assumption. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval