proposition: Theorem Xderive_pt_sin : forall f f' x, Xderive_pt f x f' -> Xderive_pt (fun x => Xsin (f x)) x (Xmul f' (Xcos (f x))).
proof: Proof. intros f f' x Hf. xtotal. intro v. apply derivable_pt_lim_eq_locally with (comp sin (proj_fun v f)). apply locally_true_imp with (2 := derivable_imp_defined_any _ _ _ _ X Hf). intros x (w, Hw). unfold comp, proj_fun. now rewrite Hw. rewrite Rmult_comm. apply derivable_pt_lim_comp. apply Hf. unfold proj_fun. rewrite X. apply derivable_pt_lim_sin. Qed.
imports: Coq(Reals) Flocq(Raux) Stdlib Xreal