proposition: Lemma arcsinh_lt : forall x y, x < y -> arcsinh x < arcsinh y.
proof: Proof. intros x y xy. case (Rle_dec (arcsinh y) (arcsinh x));[ | apply Rnot_le_lt ]. intros abs; case (Rlt_not_le _ _ xy). rewrite <- (sinh_arcsinh y), <- (sinh_arcsinh x). destruct abs as [lt | q];[| rewrite q; lra]. apply Rlt_le, sinh_lt; assumption. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra