proposition: Theorem sin_gt_0 : forall x:R, 0 < x -> x < PI -> 0 < sin x.
proof: Proof. intros; elim (SIN x (Rlt_le 0 x H) (Rlt_le x PI H0)); intros H1 _; case (Rtotal_order x (PI / 2)); intro H2. - apply Rlt_le_trans with (sin_lb x). + apply sin_lb_gt_0; [ assumption | left; assumption ]. + assumption. - elim H2; intro H3. + rewrite H3; rewrite sin_PI2; apply Rlt_0_1. + rewrite <- sin_PI_x; generalize (Ropp_gt_lt_contravar x (PI / 2) H3); intro H4; generalize (Rplus_lt_compat_l PI (- x) (- (PI / 2)) H4). replace (PI + - (PI / 2)) with (PI / 2) by field. intro H5; generalize (Ropp_lt_gt_contravar x PI H0); intro H6; change (- PI < - x) in H6; generalize (Rplus_lt_compat_l PI (- PI) (- x) H6). rewrite Rplus_opp_r. intro H7; elim (SIN (PI - x) (Rlt_le 0 (PI - x) H7) (Rlt_le (PI - x) PI (Rlt_trans (PI - x) (PI / 2) PI H5 PI2_Rlt_PI))); intros H8 _; generalize (sin_lb_gt_0 (PI - x) H7 (Rlt_le (PI - x) (PI / 2) H5)); intro H9; apply (Rlt_le_trans 0 (sin_lb (PI - x)) (sin (PI - x)) H9 H8). 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