proposition: Lemma sin_first_order : forall x, 0 <= x -> sin x <= x.
proof: Proof. intros x xpos ; apply Rle_Rminus_rev ; pose (g := (id - sin)%F). transitivity (g 0) ; [unfold g, minus_fct, id ; rewrite sin_0, Rminus_0_r ; reflexivity |]. transitivity (g x) ; [| reflexivity]. assert (Hg : derivable g). unfold g ; apply derivable_minus ; [apply derivable_id | intro a ; apply sin_derivable]. eapply nonneg_derivative_1 with Hg ; [| eassumption]. clear ; intro x ; erewrite derive_pt_minus with (prg := sin_derivable x) (prf := derivable_pt_id x), derive_pt_id, derive_pt_sin. apply Rle_Rminus, cos_bound. 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