proposition: Lemma arcsinh_le : forall x y, x <= y -> arcsinh x <= arcsinh y.
proof: Proof. intros x y [xy | xqy]. - apply Rlt_le, arcsinh_lt; assumption. - rewrite xqy; apply Rle_refl. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra