proposition: Lemma sin_bound : forall x, interval (- 1) 1 (sin x).
proof: Proof. intro x ; destruct (Rle_lt_dec (sin x) 1) as [Hub | Hf]. destruct (Rle_lt_dec (- 1) (sin x)) as [Hlb | Hf]. split ; assumption. destruct (Rlt_irrefl 1) ; apply Rle_lt_trans with ((-(1))² + (cos x)²). rewrite <- Rsqr_neg, Rsqr_1 ; apply Rplus_le_simpl_l, Rle_0_sqr. apply Rlt_le_trans with ((sin x)² + (cos x)²). apply Rplus_lt_compat_r, sqr_lt_switch ; lra. right ; apply sin2_cos2. destruct (Rlt_irrefl 1) ; apply Rle_lt_trans with (1² + (cos x)²). rewrite Rsqr_1 ; apply Rplus_le_simpl_l, Rle_0_sqr. apply Rlt_le_trans with ((sin x)² + (cos x)²). apply Rplus_lt_compat_r, Rsqr_incrst_1 ; lra. right ; apply sin2_cos2. 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