proposition: Lemma IVT'_inc : forall I F, Continuous I F -> forall a b Ha Hb, F a Ha [#] F b Hb -> I a -> I b -> (forall x y, I x -> I y -> x [<] y -> forall Hx Hy, F x Hx [<] F y Hy) -> forall y, olor (Min (F a Ha) (F b Hb)) (Max (F a Ha) (F b Hb)) y -> {x : IR | olor (Min a b) (Max a b) x | forall Hx, F x Hx [=] y}.
proof: Proof. intros I F H a b Ha Hb H0 H1 H2 H3 y H4. set (H5 := pfstrx _ _ _ _ _ _ H0) in *. elim (ap_imp_less _ _ _ H5); clear H5; intro. cut (Continuous_I (Min_leEq_Max a b) F). intro H5. 2: apply included_imp_Continuous with I; auto; apply included_interval; auto. cut (Min a b [=] a); [ intro | apply leEq_imp_Min_is_lft; apply less_leEq; auto ]. cut (Max a b [=] b); [ intro | apply leEq_imp_Max_is_rht; apply less_leEq; auto ]. cut (forall H H', F (Min a b) H [<] F (Max a b) H'). intro H8. 2: apply H3; auto. 2: apply iprop_wd with a; algebra. 2: apply iprop_wd with b; algebra. 2: astepl a; astepr b; auto. elim H4; intros. apply IVT'_I with (Min_leEq_Max a b) H5. apply ap_imp_Min_less_Max; apply less_imp_ap; auto. intros. apply H3; auto. apply (included_interval _ _ _ H1 H2 (Min_leEq_Max a b)); auto. apply (included_interval _ _ _ H1 H2 (Min_leEq_Max a b)); auto. eapply less_wdl. apply a1. astepr (F a Ha); apply leEq_imp_Min_is_lft; apply less_leEq; auto. eapply less_wdr. apply b0. astepr (F b Hb); apply leEq_imp_Max_is_rht; apply less_leEq; auto. cut (Continuous_I (Min_leEq_Max b a) F). intro H5. 2: apply included_imp_Continuous with I; auto; apply included_interval; auto. cut (Min b a [=] b); [ intro | apply leEq_imp_Min_is_lft; apply less_leEq; auto ]. cut (Max b a [=] a); [ intro | apply leEq_imp_Max_is_rht; apply less_leEq; auto ]. cut (forall H H', F (Min b a) H [<] F (Max b a) H'). intro H8. 2: apply H3; auto. 2: apply iprop_wd with b; algebra. 2: apply iprop_wd with a; algebra. 2: astepl b; astepr a; auto. elim H4; intros. elim IVT'_I with (contF := H5) (z := y); auto. intros x H9 H10; exists x; auto. elim H9; clear H9; intros H11 H12; split. eapply less_wdl; [ apply H11 | apply Min_comm ]. eapply less_wdr; [ apply H12 | apply Max_comm ]. apply ap_imp_Min_less_Max; apply less_imp_ap; auto. intros; apply H3; auto. apply (included_interval _ _ _ H2 H1 (Min_leEq_Max b a)); auto. apply (included_interval _ _ _ H2 H1 (Min_leEq_Max b a)); auto. eapply less_wdl. apply a0. astepr (F b Hb); eapply eq_transitive_unfolded. apply Min_comm. apply leEq_imp_Min_is_lft; apply less_leEq; auto. eapply less_wdr. apply b1. astepr (F a Ha); eapply eq_transitive_unfolded. apply Max_comm. apply leEq_imp_Max_is_rht; apply less_leEq; auto. Qed.
imports: CoRN.ftc.WeakIVT CoRN.ftc.CalculusTheorems