proposition: Lemma SIN_bound : forall x:R, -1 <= sin x <= 1.
proof: Proof. intro; destruct (Rle_dec (-1) (sin x)) as [Hle|Hnle]. - destruct (Rle_dec (sin x) 1) as [Hle'|Hnle']. + split; assumption. + cut (1 < sin x). * intro; generalize (Rsqr_incrst_1 1 (sin x) H (Rlt_le 0 1 Rlt_0_1) (Rlt_le 0 (sin x) (Rlt_trans 0 1 (sin x) Rlt_0_1 H))); rewrite Rsqr_1; intro; rewrite sin2 in H0; unfold Rminus in H0. generalize (Rplus_lt_compat_l (-1) 1 (1 + - Rsqr (cos x)) H0); repeat rewrite <- Rplus_assoc; change (-1) with (-(1)); rewrite Rplus_opp_l; rewrite Rplus_0_l; intro; rewrite <- Ropp_0 in H1; generalize (Ropp_lt_gt_contravar (-0) (- Rsqr (cos x)) H1); repeat rewrite Ropp_involutive; intro; generalize (Rle_0_sqr (cos x)); intro; elim (Rlt_irrefl 0 (Rle_lt_trans 0 (Rsqr (cos x)) 0 H3 H2)). * auto with real. - cut (sin x < -1). + intro; generalize (Ropp_lt_gt_contravar (sin x) (-1) H); change (-1) with (-(1)); rewrite Ropp_involutive; clear H; intro; generalize (Rsqr_incrst_1 1 (- sin x) H (Rlt_le 0 1 Rlt_0_1) (Rlt_le 0 (- sin x) (Rlt_trans 0 1 (- sin x) Rlt_0_1 H))); rewrite Rsqr_1; intro; rewrite <- Rsqr_neg in H0; rewrite sin2 in H0; unfold Rminus in H0; generalize (Rplus_lt_compat_l (-1) 1 (1 + - Rsqr (cos x)) H0); rewrite <- Rplus_assoc; change (-1) with (-(1)); rewrite Rplus_opp_l; rewrite Rplus_0_l; intro; rewrite <- Ropp_0 in H1; generalize (Ropp_lt_gt_contravar (-0) (- Rsqr (cos x)) H1); repeat rewrite Ropp_involutive; intro; generalize (Rle_0_sqr (cos x)); intro; elim (Rlt_irrefl 0 (Rle_lt_trans 0 (Rsqr (cos x)) 0 H3 H2)). + auto with real. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Rtrigo_def Rtrigo_alt Cos_rel Cos_plus ZArith_base Zcomplements Lia Lra Ranalysis1 Rsqrt_def PSeries_reg