proposition: Lemma sinh_arcsinh x : sinh (arcsinh x) = x.
proof: Proof. unfold sinh, arcsinh. assert (cmp : 0 < x + sqrt (x ^ 2 + 1)). { destruct (Rle_dec x 0). - 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;[reflexivity | lra]. - apply Rplus_lt_le_0_compat;[apply Rnot_le_gt; assumption | apply sqrt_pos]. } rewrite exp_ln;[ | assumption]. rewrite exp_Ropp, exp_ln;[ | assumption]. assert (Rmult_minus_distr_r : forall x y z, (x - y) * z = x * z - y * z) by (intros; ring). apply Rminus_diag_uniq; unfold Rdiv; rewrite Rmult_minus_distr_r. assert (t: forall x y z, x - z = y -> x - y - z = 0);[ | apply t; clear t]. - intros a b c H; rewrite <- H; ring. - apply Rmult_eq_reg_l with (2 * (x + sqrt (x ^ 2 + 1)));[ | apply Rgt_not_eq, Rmult_lt_0_compat;[apply Rlt_0_2 | assumption]]. field_simplify;[rewrite pow2_sqrt;[field | ] | apply Rgt_not_eq; lra]. apply Rplus_le_le_0_compat;[simpl; rewrite Rmult_1_r; apply (Rle_0_sqr x)|apply Rlt_le, Rlt_0_1]. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra