proposition: Lemma IVT_I : {x : IR | I x | forall Hx, F x Hx [=] z}.
proof: Proof. exists xa. apply xa_in_interval. intro. apply cg_inv_unique_2; apply leEq_imp_eq. apply approach_zero. intros e H. apply leEq_less_trans with (e [/]TwoNZ). 2: apply pos_div_two'; auto. elim (contin_prop _ _ _ _ contF _ (pos_div_two _ _ H)); intros d H0 H1. elim (Cauchy_complete (Build_CauchySeq _ _ a_seq_Cauchy) _ H0); fold xa in |- *; simpl in |- *; intros N HN. apply leEq_transitive with (F xa Hx[-]F (a_seq N) (incF _ (a_seq_I N))). unfold cg_minus in |- *; apply plus_resp_leEq_lft. apply inv_resp_leEq; apply a_seq_leEq_z. eapply leEq_wdl. 2: apply AbsIR_eq_x. apply H1; auto. apply xa_in_interval. apply a_seq_I. apply AbsSmall_imp_AbsIR. apply AbsSmall_minus. auto. apply shift_leEq_minus; astepl (F _ (incF _ (a_seq_I N))). apply part_mon_imp_mon' with I; auto. apply a_seq_I. apply xa_in_interval. unfold xa in |- *. apply str_leEq_seq_so_leEq_Lim. exists N; intros; simpl in |- *. apply local_mon'_imp_mon'; auto; exact a_seq_mon. astepl ( [--]ZeroR); rstepr ( [--] (z[-]F xa Hx)). apply inv_resp_leEq. apply approach_zero. intros e H. apply leEq_less_trans with (e [/]TwoNZ). 2: apply pos_div_two'; auto. elim (contin_prop _ _ _ _ contF _ (pos_div_two _ _ H)); intros d H0 H1. elim (Cauchy_complete (Build_CauchySeq _ _ b_seq_Cauchy) _ H0); fold xb in |- *; simpl in |- *; intros N HN. apply leEq_transitive with (F (b_seq N) (incF _ (b_seq_I N)) [-]F xa Hx). apply minus_resp_leEq; apply z_leEq_b_seq. eapply leEq_wdl. 2: apply AbsIR_eq_x. apply H1; auto. apply b_seq_I. apply xa_in_interval. apply leEq_wdl with (AbsIR (b_seq N[-]xb)). 2: apply AbsIR_wd; apply cg_minus_wd; [ algebra | apply eq_symmetric_unfolded; apply a_seq_b_seq_lim ]. apply AbsSmall_imp_AbsIR. auto. apply shift_leEq_minus; astepl (F xa Hx). apply part_mon_imp_mon' with I; auto. apply xa_in_interval. apply b_seq_I. apply leEq_wdl with xb. 2: apply eq_symmetric_unfolded; apply a_seq_b_seq_lim. unfold xb in |- *. apply str_seq_leEq_so_Lim_leEq. exists N; intros; simpl in |- *. astepl ( [--][--] (b_seq i)); astepr ( [--][--] (b_seq N)). apply inv_resp_leEq. apply local_mon'_imp_mon' with (f := fun n : nat => [--] (b_seq n)); auto. intro; apply inv_resp_leEq; apply b_seq_mon. Qed.
imports: CoRN.ftc.Continuity