proposition: Lemma derivable_pt_lim_cosh : forall x:R, derivable_pt_lim cosh x (sinh x).
proof: Proof. intro. unfold cosh, sinh; unfold Rdiv. replace (fun x0:R => (exp x0 + exp (- x0)) * / 2) with ((exp + comp exp (- id)) * fct_cte (/ 2))%F; [ idtac | reflexivity ]. replace ((exp x - exp (- x)) * / 2) with ((exp x + exp (- x) * -1) * fct_cte (/ 2) x + (exp + comp exp (- id))%F x * 0). - apply derivable_pt_lim_mult. + apply derivable_pt_lim_plus. * apply derivable_pt_lim_exp. * apply derivable_pt_lim_comp. -- apply derivable_pt_lim_opp. apply derivable_pt_lim_id. -- apply derivable_pt_lim_exp. + apply derivable_pt_lim_const. - unfold plus_fct, mult_real_fct, comp, opp_fct, id, fct_cte; ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Ranalysis3 Exp_prop MVT Lra Lia