proposition: Lemma f_interv_is_interv : forall (f:R->R) (lb ub y:R), lb < ub -> f lb <= y <= f ub -> (forall x, lb <= x <= ub -> continuity_pt f x) -> {x | lb <= x <= ub /\ f x = y}.
proof: Proof. intros f lb ub y lb_lt_ub y_encad f_cont_interv. case y_encad ; intro y_encad1. case_le y_encad1 ; intros y_encad2 y_encad3 ; case_le y_encad3. - intro y_encad4. clear y_encad y_encad1 y_encad3. assert (Cont : forall a : R, lb <= a <= ub -> continuity_pt (fun x => f x - y) a). { intros a a_encad. unfold continuity_pt, continue_in, limit1_in, limit_in ; simpl ; unfold Rdist. intros eps eps_pos. elim (f_cont_interv a a_encad eps eps_pos). intros alpha alpha_pos. destruct alpha_pos as (alpha_pos,Temp). exists alpha. split. { assumption. } intros x x_cond. replace (f x - y - (f a - y)) with (f x - f a) by field. exact (Temp x x_cond). } assert (H1 : (fun x : R => f x - y) lb < 0). { apply Rlt_minus. assumption. } assert (H2 : 0 < (fun x : R => f x - y) ub). { apply Rgt_minus ; assumption. } destruct (IVT_interv (fun x => f x - y) lb ub Cont lb_lt_ub H1 H2) as (x,Hx). exists x. destruct Hx as (Hyp,Result). intuition. - intro H ; exists ub ; intuition. - intro H ; exists lb ; intuition. - intro H ; exists ub ; intuition. Qed.
imports: Rbase Ranalysis_reg Rfunctions Rseries RiemannInt SeqProp Lia Lra