Exponential series

[affeldt-aist]

extracted from PR #207 for tentative application in coq-robot

@thery

[affeldt-aist]

I take the opportunity of this conversation to ask a related question. Given the exponential function defined as:

Definition exp (x : R) : R := lim (series (exp_coeff x)).

How to define the natural logarithm? What is better than the following?

Definition ln (R : realType) (x : R) :=
  if pselect (exists y, exp y = x) is left e then projT1 (cid e) else 0.

@CohenCyril

[affeldt-aist]

Is it ok to merge this as it is for 0.3.8 and come back to it later? @CohenCyril @thery

[CohenCyril]

OK to merge after rebase.