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