proposition: Lemma tan_reciprocal_image_interval : forall lb ub y, open_interval (- PI / 2) (PI / 2) lb -> open_interval (- PI / 2) (PI / 2) ub -> interval (tan lb) (tan ub) y -> { x | interval lb ub x /\ tan x = y }.
proof: Proof. intros lb ub y lb_in ub_in y_bd. assert (Hbd: lb <= ub). eapply strictly_increasing_interval_order ; try eassumption. eapply strictly_increasing_open_interval_tan. eapply interval_inhabited ; eassumption. destruct (interval_open_interval_dec _ _ _ y_bd) as [l | yeq]. destruct l as [yeq | y_in]. exists lb ; split ; [apply interval_l | symmetry] ; assumption. destruct (tan_reciprocal_image_open_interval _ _ _ lb_in ub_in y_in) as [z [z_in Hz]] ; exists z ; split ; [apply open_interval_interval |] ; assumption. exists ub ; split ; [apply interval_r | symmetry] ; 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