proposition: Lemma tan_reciprocal_image_open_interval : forall lb ub y, open_interval (- PI / 2) (PI / 2) lb -> open_interval (- PI / 2) (PI / 2) ub -> open_interval (tan lb) (tan ub) y -> { x | open_interval lb ub x /\ tan x = y }.
proof: Proof. intros lb ub y lb_in ub_in y_in ; apply IVT_open_interval. eapply continuity_in_contravariant ; try (eapply interval_open_restriction ; eassumption). apply continuity_open_interval_tan. eapply strictly_increasing_open_interval_order ; try eassumption. apply strictly_increasing_open_interval_tan. eapply open_interval_inhabited ; eassumption. 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