proposition: Lemma fun_const_Lim : forall J f F contf contF, proper J -> conv_fun_seq'_IR J f F contf contF -> (forall n, {c : IR | Feq J (f n) [-C-]c}) -> {c : IR | Feq J F [-C-]c}.
proof: Proof. intros J f F contf contF pJ H H0. set (incF := Continuous_imp_inc _ _ contF) in *. set (incf := fun n : nat => Continuous_imp_inc _ _ (contf n)) in *. elim (nonvoid_point _ (proper_nonvoid _ pJ)); intros x0 Hx0. exists (Part F x0 (incF x0 Hx0)). FEQ. rename X into H1. simpl in |- *. apply cg_inv_unique_2; apply AbsIR_approach_zero. intros e H2. cut (included (Compact (Min_leEq_Max x x0)) J). 2: apply included_interval; auto. intro Hinc. elim (H _ _ _ Hinc _ (pos_div_two _ _ H2)); intros N HN. set (Fx := Part _ _ Hx) in *. set (Fa := Part _ _ (incF x0 Hx0)) in *. set (fx := Part _ _ (incf N x H1)) in *. set (fa := Part _ _ (incf N x0 Hx0)) in *. apply leEq_wdl with (AbsIR (Fx[-]fx[+] (fx[-]fa) [+] (fa[-]Fa))). 2: apply AbsIR_wd; rational. rstepr (e [/]TwoNZ[+][0][+]e [/]TwoNZ). eapply leEq_transitive. apply triangle_IR. apply plus_resp_leEq_both. eapply leEq_transitive. apply triangle_IR. apply plus_resp_leEq_both. eapply leEq_wdl. 2: apply AbsIR_minus. eapply leEq_wdl. apply (HN N (le_n N) x (compact_Min_lft _ _ _)). unfold Fx, fx in |- *; apply AbsIR_wd; rational. elim (H0 N); intros c Hc. apply eq_imp_leEq. eapply eq_transitive_unfolded. 2: apply AbsIRz_isz. elim Hc; clear Hc; intros H5 H3. elim H3; clear H3; intros H6 H4. apply AbsIR_wd; unfold fx, fa in |- *; astepr (c[-]c). apply cg_minus_wd; simpl in H4; apply H4; auto. eapply leEq_wdl. apply (HN N (le_n N) x0 (compact_Min_rht _ _ _)). unfold Fa, fa in |- *; apply AbsIR_wd; rational. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions