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