proposition: Lemma arcsinh_0 : arcsinh 0 = 0.
proof: Proof. unfold arcsinh; rewrite pow_ne_zero, !Rplus_0_l, sqrt_1, ln_1; [reflexivity | discriminate]. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra