proposition: Lemma exists_atan : forall y : R, { x | open_interval (- PI / 2) (PI / 2) x /\ tan x = y }.
proof: Proof. intro y ; destruct (tan_cv_neg_infty y) as [lb [lb_in Hlb]] ; destruct (tan_cv_pos_infty y) as [ub [ub_in Hub]] ; assert (y_in : open_interval (tan lb) (tan ub) y) by (split ; assumption) ; destruct (tan_reciprocal_image_open_interval _ _ _ lb_in ub_in y_in) as [x [x_in Hx]] ; exists x ; split. eapply open_interval_restriction ; try eassumption ; eapply open_interval_interval ; assumption. 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