proposition: Lemma is_derive_sin x : is_derive sin x (cos x).
proof: Proof. apply is_derive_Reals. apply derivable_pt_lim_sin. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis