proposition: Theorem ln_inv : forall x y:R, 0 < x -> 0 < y -> ln x = ln y -> x = y.
proof: Proof. intros x y H H0 H'0; case (Rtotal_order x y); [ intros H1 | intros [H1| H1] ]; auto. - assert (H2 := ln_increasing _ _ H H1); rewrite H'0 in H2; elim (Rlt_irrefl _ H2). - assert (H2 := ln_increasing _ _ H0 H1); rewrite H'0 in H2; elim (Rlt_irrefl _ H2). Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra