proposition: Lemma strictly_increasing_interval_sin : strictly_increasing_interval (- PI / 2) (PI / 2) sin.
proof: Proof. replace (- PI / 2) with (- (PI / 2)) by field. do 5 intro ; apply sin_increasing_1 ; eapply_assumption. Qed.
imports: Rbase Rtactic Lra Ranalysis Ranalysis5 Rtrigo AltSeries Rfunctions Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Rextensionality Rpser_usual Rsequence_cv_facts MyRIneq Tactics