proposition: Lemma derive_pt_sinh : forall x:R, derive_pt sinh x (derivable_pt_sinh x) = cosh x.
proof: Proof. intro; apply derive_pt_eq_0. apply derivable_pt_lim_sinh. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Ranalysis3 Exp_prop MVT Lra Lia