proposition: Lemma tan_cv_pos_infty : forall y , { x | open_interval (- PI / 2) (PI / 2) x /\ y < tan x }.
proof: Proof. intro y ; destruct (Req_dec y 0) as [y_eq | y_neq]. exists (PI / 4) ; split ; [exact PI4_in |] ; subst ; apply tan_gt_0 ; [apply PI4_RGT_0 | apply PI4_RLT_PI2]. assert (y_pos : 0 < Rabs y) by (apply Rabs_pos_lt ; assumption) ; destruct (tan_cv_pos_infty_prelim _ y_pos) as [x [x_in Hx]] ; exists x ; split ; [| apply Rgt_ge_trans with (Rabs y), Rle_ge, Rle_abs] ; 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