proposition: Lemma sin_lb_gt_0 : forall a:R, 0 < a -> a <= PI / 2 -> 0 < sin_lb a.
proof: Proof. intros. unfold sin_lb in |- *; unfold sin_approx in |- *; unfold sin_term in |- *. set (Un := fun i:nat => a ^ (2 * i + 1) / INR (fact (2 * i + 1))). replace (sum_f_R0 (fun i:nat => (-1) ^ i * (a ^ (2 * i + 1) / INR (fact (2 * i + 1)))) 3) with (sum_f_R0 (fun i:nat => (-1) ^ i * Un i) 3); [ idtac | apply sum_eq; intros; unfold Un in |- *; reflexivity ]. cut (forall n:nat, Un (S n) < Un n). { intro; simpl in |- *. repeat rewrite Rmult_1_l; repeat rewrite Rmult_1_r; replace (-1 * Un 1%nat) with (- Un 1%nat); [ idtac | ring ]; replace (-1 * -1 * Un 2%nat) with (Un 2%nat); [ idtac | ring ]; replace (-1 * (-1 * -1) * Un 3%nat) with (- Un 3%nat); [ idtac | ring ]; replace (Un 0%nat + - Un 1%nat + Un 2%nat + - Un 3%nat) with (Un 0%nat - Un 1%nat + (Un 2%nat - Un 3%nat)); [ idtac | ring ]. apply Rplus_lt_0_compat. - unfold Rminus in |- *; apply Rplus_lt_reg_l with (Un 1%nat); rewrite Rplus_0_r; rewrite (Rplus_comm (Un 1%nat)); rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; apply H1. - unfold Rminus in |- *; apply Rplus_lt_reg_l with (Un 3%nat); rewrite Rplus_0_r; rewrite (Rplus_comm (Un 3%nat)); rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; apply H1. } intro; unfold Un in |- *. assert ((2 * S n + 1)%nat = (2 * n + 1 + 2)%nat) by ring. rewrite H1. rewrite pow_add; unfold Rdiv in |- *; rewrite Rmult_assoc; apply Rmult_lt_compat_l. { apply pow_lt; assumption. } rewrite <- H1; apply Rmult_lt_reg_l with (INR (fact (2 * n + 1))). { apply INR_fact_lt_0. } rewrite Rinv_r. 2:{ apply INR_fact_neq_0. } apply Rmult_lt_reg_l with (INR (fact (2 * S n + 1))). { apply INR_fact_lt_0. } rewrite (Rmult_comm (INR (fact (2 * S n + 1)))); repeat rewrite Rmult_assoc; rewrite Rinv_l. 2:{ apply INR_fact_neq_0. } do 2 rewrite Rmult_1_r; apply Rle_lt_trans with (INR (fact (2 * n + 1)) * 4). { apply Rmult_le_compat_l. { apply pos_INR. } simpl in |- *; rewrite Rmult_1_r; change 4 with (Rsqr 2); apply Rsqr_incr_1;[|lra|lra]. apply Rle_trans with (PI / 2); [ assumption | unfold Rdiv in |- *; apply Rmult_le_reg_l with 2; [ prove_sup0 | rewrite <- Rmult_assoc; rewrite Rmult_inv_r_id_m; [ apply PI_4 | discrR ] ] ]. } rewrite H1; replace (2 * n + 1 + 2)%nat with (S (S (2 * n + 1))) by ring. do 2 rewrite fact_simpl; do 2 rewrite mult_INR. repeat rewrite <- Rmult_assoc. rewrite <- (Rmult_comm (INR (fact (2 * n + 1)))). apply Rmult_lt_compat_l. { apply INR_fact_lt_0. } do 2 rewrite S_INR; rewrite plus_INR; rewrite mult_INR; set (x := INR n); unfold INR in |- *. pose proof (pos_INR _ : 0 <= x). nra. 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