proposition: Lemma derivable_pt_lim_cos : forall x:R, derivable_pt_lim cos x (- sin x).
proof: Proof. intro; cut (forall h:R, sin (h + PI / 2) = cos h). - intro; replace (- sin x) with (cos (x + PI / 2) * (1 + 0)). + generalize (derivable_pt_lim_comp (id + fct_cte (PI / 2))%F sin); intros. cut (derivable_pt_lim (id + fct_cte (PI / 2)) x (1 + 0)). * cut (derivable_pt_lim sin ((id + fct_cte (PI / 2))%F x) (cos (x + PI / 2))). -- intros; generalize (H0 _ _ _ H2 H1); replace (comp sin (id + fct_cte (PI / 2))%F) with (fun x:R => sin (x + PI / 2)); [ idtac | reflexivity ]. unfold derivable_pt_lim; intros. elim (H3 eps H4); intros. exists x0. intros; rewrite <- (H (x + h)); rewrite <- (H x); apply H5; assumption. -- apply derivable_pt_lim_sin. * apply derivable_pt_lim_plus. -- apply derivable_pt_lim_id. -- apply derivable_pt_lim_const. + rewrite sin_cos; rewrite <- (Rplus_comm x); ring. - intro; rewrite cos_sin; rewrite Rplus_comm; reflexivity. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lra