proposition: Lemma strictly_increasing_open_interval_atan : forall x y, open_interval (- PI / 2) (PI / 2) x -> open_interval (- PI / 2) (PI / 2) y -> tan x < tan y -> x < y.
proof: Proof. intros x y x_in y_in Hxy ; destruct (total_order_T x y) as [[Hlt | Heq] | Hgt]. assumption. subst ; destruct (Rlt_irrefl _ Hxy). destruct (Rlt_irrefl (tan x)) ; transitivity (tan y). assumption. apply strictly_increasing_open_interval_tan ; 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