proposition: Lemma exists_atan_in_frame : forall lb ub y, lb < ub -> -PI/2 < lb -> ub < PI/2 -> tan lb < y < tan ub -> {x | lb < x < ub /\ tan x = y}.
proof: Proof. intros lb ub y lb_lt_ub lb_cond ub_cond y_encad. case y_encad ; intros y_encad1 y_encad2. assert (f_cont : forall a : R, lb <= a <= ub -> continuity_pt tan a). { intros a a_encad. apply derivable_continuous_pt ; apply derivable_pt_tan. split. - apply Rlt_le_trans with (r2:=lb) ; intuition. - apply Rle_lt_trans with (r2:=ub) ; intuition. } assert (Cont : forall a : R, lb <= a <= ub -> continuity_pt (fun x => tan 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 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 (tan x - y - (tan a - y)) with (tan x - tan a) by field. exact (Temp x x_cond). } assert (H1 : (fun x => tan x - y) lb < 0). { apply Rlt_minus. assumption. } assert (H2 : 0 < (fun x => tan x - y) ub). { apply Rgt_minus. assumption. } destruct (IVT_interv (fun x => tan x - y) lb ub Cont lb_lt_ub H1 H2) as (x,Hx). exists x. destruct Hx as (Hyp,Result). intuition. - assert (Temp2 : x <> lb). { intro Hfalse. rewrite Hfalse in Result. assert (Temp2 : y <> tan lb) by (now apply Rgt_not_eq, Rlt_minus_0). rewrite Result in H1. now apply (Rlt_irrefl 0). } now case H3; intros hyp; [assumption |]; rewrite hyp in Temp2. - assert (Temp : x <> ub). { intro Hfalse. rewrite Hfalse in Result. assert (Temp2 : y <> tan ub). { apply Rlt_not_eq ; assumption. } clear - Temp2 Result. apply Temp2. symmetry; intuition. } case H4 ; intuition. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia