proposition: Lemma IVT : forall (f:R -> R) (x y:R), continuity f -> x < y -> f x < 0 -> 0 < f y -> { z:R | x <= z <= y /\ f z = 0 }.
proof: Proof. intros. assert (x <= y) by (left; assumption). destruct (dicho_lb_cv x y (fun z:R => cond_positivity (f z)) H3) as (x1,p0). destruct (dicho_up_cv x y (fun z:R => cond_positivity (f z)) H3) as (x0,p). assert (H4 := cv_dicho _ _ _ _ _ H3 p0 p). rewrite H4 in p0. exists x0. split;[split|]. - apply Rle_trans with (dicho_lb x y (fun z:R => cond_positivity (f z)) 0). { simpl. right; reflexivity. } apply growing_ineq. { apply dicho_lb_growing; assumption. } assumption. - apply Rle_trans with (dicho_up x y (fun z:R => cond_positivity (f z)) 0). { apply decreasing_ineq. { apply dicho_up_decreasing; assumption. } assumption. } right; reflexivity. - set (Vn := fun n:nat => dicho_lb x y (fun z:R => cond_positivity (f z)) n). set (Wn := fun n:nat => dicho_up x y (fun z:R => cond_positivity (f z)) n). cut ((forall n:nat, f (Vn n) <= 0) -> f x0 <= 0). 1:cut ((forall n:nat, 0 <= f (Wn n)) -> 0 <= f x0). + intros. cut (forall n:nat, f (Vn n) <= 0). 1:cut (forall n:nat, 0 <= f (Wn n)). { intros. assert (H9 := H6 H8). assert (H10 := H5 H7). apply Rle_antisym; assumption. } * intro. unfold Wn. cut (forall z:R, cond_positivity z = true <-> 0 <= z). 2:{ intro. unfold cond_positivity. case (Rle_dec 0 z) as [Hle|Hnle]. - split. + intro; assumption. + intro; reflexivity. - split. + intro feqt;discriminate feqt. + intro. contradiction. } intro. assert (H8 := dicho_up_car x y (fun z:R => cond_positivity (f z)) n). elim (H7 (f (dicho_up x y (fun z:R => cond_positivity (f z)) n))); intros. apply H9. apply H8. elim (H7 (f y)); intros. apply H12. left; assumption. * unfold Vn. cut (forall z:R, cond_positivity z = false <-> z < 0). 2:{ intro. unfold cond_positivity. case (Rle_dec 0 z) as [Hle|Hnle]. - split. + intro feqt; discriminate feqt. + intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle H7)). - split. + intro; auto with real. + intro; reflexivity. } intros. assert (H8 := dicho_lb_car x y (fun z:R => cond_positivity (f z)) n). left. elim (H7 (f (dicho_lb x y (fun z:R => cond_positivity (f z)) n))); intros. apply H9. apply H8. elim (H7 (f x)); intros. apply H12. assumption. + assert (Un_cv Wn x0) by (unfold Wn; assumption). intros. assert (H7 := continuity_seq f Wn x0 (H x0) H5). destruct (total_order_T 0 (f x0)) as [[Hlt|<-]|Hgt]. { left; assumption. } { right; reflexivity. } unfold Un_cv in H7; unfold Rdist in H7. assert (0 < - f x0) by (apply Ropp_0_gt_lt_contravar; assumption). elim (H7 (- f x0) H8); intros. cut (x2 >= x2)%nat; [ intro | unfold ge; apply le_n ]. assert (H11 := H9 x2 H10). rewrite Rabs_right in H11. 2:{ apply Rle_ge; left; unfold Rminus; apply Rplus_le_lt_0_compat. - apply H6. - exact H8. } pattern (- f x0) at 1 in H11; rewrite <- Rplus_0_r in H11. unfold Rminus in H11; rewrite (Rplus_comm (f (Wn x2))) in H11. assert (H12 := Rplus_lt_reg_l _ _ _ H11). assert (H13 := H6 x2). elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H13 H12)). + assert (Un_cv Vn x0) by (unfold Vn; assumption). intros. assert (H7 := continuity_seq f Vn x0 (H x0) H5). destruct (total_order_T 0 (f x0)) as [[Hlt|<-]|Hgt]. 2:{ right; reflexivity. } 2:{ left; assumption. } unfold Un_cv in H7; unfold Rdist in H7. elim (H7 (f x0) Hlt); intros. cut (x2 >= x2)%nat; [ intro | unfold ge; apply le_n ]. assert (H10 := H8 x2 H9). rewrite Rabs_left in H10. 2:{ apply Rplus_lt_reg_l with (f x0 - f (Vn x2)). rewrite Rplus_0_r; replace (f x0 - f (Vn x2) + (f (Vn x2) - f x0)) with 0; [ unfold Rminus; apply Rplus_lt_le_0_compat | ring ]. - assumption. - apply Ropp_0_ge_le_contravar; apply Rle_ge; apply H6. } pattern (f x0) at 2 in H10; rewrite <- Rplus_0_r in H10. rewrite Ropp_minus_distr in H10. unfold Rminus in H10. assert (H11 := Rplus_lt_reg_l _ _ _ H10). assert (H12 := H6 x2). cut (0 < f (Vn x2)). * intro. elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H13 H12)). * rewrite <- (Ropp_involutive (f (Vn x2))). apply Ropp_0_gt_lt_contravar; assumption. Qed.
imports: Sumbool Rbase Rfunctions SeqSeries Ranalysis1 Lra