proposition: Lemma tan_cv_neg_infty : forall y, { x | open_interval (- PI / 2) (PI / 2) x /\ tan x < y }.
proof: Proof. intro y ; destruct (tan_cv_pos_infty (- y)) as [x [x_in Hx]] ; exists (- x) ; split. rewrite <- (Ropp_involutive (PI /2)), Ropp_Rdiv_compat_l ; [apply open_interval_opp_compat ; rewrite <- Ropp_Rdiv_compat_l |] ; (assumption || apply Rgt_not_eq ; lra). rewrite tan_neg ; apply Ropp_lt_cancel ; rewrite Ropp_involutive ; 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