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