proposition: Lemma derivable_pt_lim_cos_0 : derivable_pt_lim cos 0 0.
proof: Proof. unfold derivable_pt_lim; intros. assert (H0 := derivable_pt_lim_sin_0). unfold derivable_pt_lim in H0. assert (0 < eps / 2) by lra. elim (H0 _ H1); intros del H2. assert (continuity_pt sin 0) by apply continuity_sin. unfold continuity_pt in H3; unfold continue_in in H3; unfold limit1_in in H3; unfold limit_in in H3; simpl in H3; unfold Rdist in H3. cut (0 < eps / 2); [ intro | assumption ]. elim (H3 _ H4); intros del_c H5. assert (0 < Rmin del del_c). { unfold Rmin; case (Rle_dec del del_c); intro. - apply (cond_pos del). - elim H5; intros; assumption. } set (delta := mkposreal _ H6). exists delta; intros. rewrite Rplus_0_l; replace (cos h - cos 0) with (-2 * Rsqr (sin (h / 2))). 2:{ pattern h at 2; replace h with (2 * (h / 2)) by field. rewrite (cos_2a_sin (h / 2)). rewrite cos_0; unfold Rsqr; ring. } unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r. change (-2) with (-(2)). unfold Rdiv; do 2 rewrite Ropp_mult_distr_l_reverse. rewrite Rabs_Ropp. replace (2 * Rsqr (sin (h * / 2)) * / h) with (sin (h / 2) * (sin (h / 2) / (h / 2) - 1) + sin (h / 2)). 2:{ rewrite Rmult_minus_distr_l; rewrite Rmult_1_r; unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; rewrite (Rmult_comm 2); unfold Rdiv, Rsqr. field. assumption. } apply Rle_lt_trans with (Rabs (sin (h / 2) * (sin (h / 2) / (h / 2) - 1)) + Rabs (sin (h / 2))). { apply Rabs_triang. } rewrite <-(Rplus_half_diag eps); apply Rplus_lt_compat. - apply Rle_lt_trans with (Rabs (sin (h / 2) / (h / 2) - 1)). { rewrite Rabs_mult; rewrite Rmult_comm; pattern (Rabs (sin (h / 2) / (h / 2) - 1)) at 2; rewrite <- Rmult_1_r; apply Rmult_le_compat_l. { apply Rabs_pos. } pose proof (SIN_bound (h/2));unfold Rabs. destruct (Rcase_abs _);lra. } cut (Rabs (h / 2) < del). { intro; assert (h / 2 <> 0) by lra. assert (H11 := H2 _ H10 H9). rewrite Rplus_0_l in H11; rewrite sin_0 in H11. rewrite Rminus_0_r in H11; apply H11. } apply Rlt_trans with (del / 2). 2:pose proof (cond_pos del);lra. unfold Rdiv; rewrite Rabs_mult. rewrite (Rabs_right (/ 2)). 2:lra. do 2 rewrite <- (Rmult_comm (/ 2)); apply Rmult_lt_compat_l. { lra. } apply Rlt_le_trans with (pos delta). { assumption. } unfold delta; simpl; apply Rmin_l. - elim H5; intros; assert (H11 := H10 (h / 2)). rewrite sin_0 in H11; do 2 rewrite Rminus_0_r in H11. apply H11. split. { unfold D_x, no_cond; split;lra. } apply Rlt_trans with (del_c / 2). 2:{ lra. } unfold Rdiv; rewrite Rabs_mult. rewrite (Rabs_right (/ 2)). 2:lra. do 2 rewrite <- (Rmult_comm (/ 2)). apply Rmult_lt_compat_l. { lra. } apply Rlt_le_trans with (pos delta). + assumption. + unfold delta; simpl; apply Rmin_r. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lra