proposition: Lemma PI4_in : open_interval (- PI / 2) (PI / 2) (PI / 4).
proof: Proof. replace (- PI / 2) with (- (PI / 2)) by field ; split. transitivity 0 ; [apply _PI2_RLT_0 | apply PI4_RGT_0]. apply PI4_RLT_PI2. 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