proposition: Lemma tan_cv_pos_infty_prelim : forall y , 0 < y -> { x | open_interval (- PI / 2) (PI / 2) x /\ y < tan x }.
proof: Proof. intros y y_pos ; destruct (cos_cv_0_left (/ (2 * y)) (PI / 6)) as [x [x_in Hx]]. apply Rinv_0_lt_compat ; lra. apply PI6_in. assert (x_bd : open_interval (- PI / 2) (PI / 2) x). eapply open_interval_restriction. eapply open_interval_interval, PI6_in. eapply interval_r ; left ; exact _PI2_Rlt_PI2. assumption. assert (cosx_pos : 0 < cos x) by (apply cos_pos ; assumption). exists x ; split ; [assumption |]. apply Rlt_le_trans with (/ (2 * cos x)). rewrite <- Rinv_involutive with y ; [apply Rinv_lt_contravar | apply Rgt_not_eq ; lra]. apply Rlt_mult_inv_pos ; [apply Rmult_lt_0_compat |] ; (assumption || lra). apply Rmult_Rinv_lt_compat_r_rev ; [| rewrite <- Rinv_mult_distr, Rmult_comm] ; (assumption || apply Rgt_not_eq || idtac) ; lra. rewrite Rinv_mult_distr ; try (apply Rgt_not_eq ; (assumption || lra)) ; apply Rmult_le_compat_r ; [left ; apply Rinv_0_lt_compat ; assumption |]. transitivity (sin (PI / 6)). right ; rewrite sin_PI6 ; unfold Rdiv ; ring. left ; apply strictly_increasing_interval_sin ; try apply open_interval_interval ; (exact PI6_in || eapply_assumption). Qed.
imports: Rbase Rtactic Lra Ranalysis Rfunctions Rtrigo_facts Rseries_def SeqProp Rextensionality Rpser_usual RIVT Rseries_facts Rsequence_cv_facts MyRIneq Tactics Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis5