proposition: Lemma sin_cv_0_right : forall eps a, 0 < eps -> 0 < a -> { x | open_interval 0 a x /\ sin x < eps }.
proof: Proof. intros eps a eps_pos a_pos ; pose (f := Rmin eps a) ; assert (f_pos : 0 < f) by (apply Rmin_pos_lt ; assumption) ; exists (f / 2) ; repeat split. apply Rlt_mult_inv_pos ; [assumption | lra]. apply Rlt_le_trans with f ; [lra | apply Rmin_r]. apply Rle_lt_trans with (f / 2) ; [apply sin_first_order | apply Rlt_le_trans with f, Rmin_l] ; lra. 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