proposition: Lemma _PI2_Rlt_PI2 : - PI / 2 < PI / 2.
proof: Proof. replace (- PI / 2) with (- (PI / 2)) by field ; transitivity 0 ; [apply _PI2_RLT_0 | apply PI2_RGT_0]. 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