proposition: Lemma ln_exists : forall y:R, 0 < y -> { z:R | y = exp z }.
proof: Proof. intros; destruct (Rle_dec 1 y) as [Hle|Hnle]. - apply (ln_exists1 _ Hle). - assert (H0 : 1 <= / y). + apply Rmult_le_reg_l with y. * apply H. * rewrite Rinv_r. -- rewrite Rmult_1_r; left; apply (Rnot_le_lt _ _ Hnle). -- red; intro; rewrite H0 in H; elim (Rlt_irrefl _ H). + destruct (ln_exists1 _ H0) as (x,p); exists (- x); apply Rmult_eq_reg_l with (exp x / y). * unfold Rdiv; rewrite Rmult_assoc; rewrite Rinv_l. -- rewrite Rmult_1_r; rewrite <- (Rmult_comm (/ y)); rewrite Rmult_assoc; rewrite <- exp_plus; rewrite Rplus_opp_r; rewrite exp_0; rewrite Rmult_1_r; symmetry ; apply p. -- red; intro H3; rewrite H3 in H; elim (Rlt_irrefl _ H). * unfold Rdiv; apply prod_neq_R0. -- assert (H3 := exp_pos x); red; intro H4; rewrite H4 in H3; elim (Rlt_irrefl _ H3). -- apply Rinv_neq_0_compat; red; intro H3; rewrite H3 in H; elim (Rlt_irrefl _ H). Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra