proposition: Lemma derivable_pt_lim_arcsinh : forall x, derivable_pt_lim arcsinh x (/sqrt (x ^ 2 + 1)).
proof: Proof. intros x; unfold arcsinh. assert (0 < x + sqrt (x ^ 2 + 1)). { destruct (Rle_dec x 0); [ | assert (0 < x) by (apply Rnot_le_gt; assumption); apply Rplus_lt_le_0_compat; auto; apply sqrt_pos]. replace (x ^ 2) with ((-x) ^ 2) by ring. assert (sqrt ((- x) ^ 2) < sqrt ((-x)^2+1)). { apply sqrt_lt_1_alt. split;[apply pow_le|]; lra. } pattern x at 1; replace x with (- (sqrt ((- x) ^ 2))). - assert (t:= sqrt_pos ((-x)^2)); lra. - simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive; auto; lra. } assert (0 < x ^ 2 + 1). { apply Rplus_le_lt_0_compat;[simpl; rewrite Rmult_1_r; apply Rle_0_sqr|lra]. } replace (/sqrt (x ^ 2 + 1)) with (/(x + sqrt (x ^ 2 + 1)) * (1 + (/(2 * sqrt (x ^ 2 + 1)) * (INR 2 * x ^ 1 + 0)))). 2:{ replace (INR 2 * x ^ 1 + 0) with (2 * x) by (simpl; ring). replace (1 + / (2 * sqrt (x ^ 2 + 1)) * (2 * x)) with (((sqrt (x ^ 2 + 1) + x))/sqrt (x ^ 2 + 1)); [ | field; apply Rgt_not_eq, sqrt_lt_R0; assumption]. apply Rmult_eq_reg_l with (x + sqrt (x ^ 2 + 1)); [ | apply Rgt_not_eq; assumption]. field. split;apply Rgt_not_eq; auto; apply sqrt_lt_R0; assumption. } apply (derivable_pt_lim_comp (fun x => x + sqrt (x ^ 2 + 1)) ln). + apply (derivable_pt_lim_plus). * apply derivable_pt_lim_id. * apply (derivable_pt_lim_comp (fun x => x ^ 2 + 1) sqrt x). -- apply derivable_pt_lim_plus. ++ apply derivable_pt_lim_pow. ++ apply derivable_pt_lim_const. -- apply derivable_pt_lim_sqrt; assumption. + apply derivable_pt_lim_ln; assumption. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra