proposition: Lemma arcsinh_sinh : forall x, arcsinh (sinh x) = x.
proof: Proof. intros x; unfold sinh, arcsinh. assert (Rminus_eq_0 : forall r, r - r = 0) by (intros; ring). rewrite <- exp_0, <- (Rminus_eq_0 x); unfold Rminus. rewrite exp_plus. match goal with |- context[sqrt ?a] => replace a with (((exp x + exp(-x))/2)^2) by field end. rewrite sqrt_pow2; [|apply Rlt_le, Rmult_lt_0_compat;[apply Rplus_lt_0_compat; apply exp_pos | apply Rinv_0_lt_compat, Rlt_0_2]]. match goal with |- context[ln ?a] => replace a with (exp x) by field end. rewrite ln_exp; reflexivity. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra