add_one_le_exp

Stream: new members

[Iván Sadofschi Costa]

Hi all! I'm new to Lean. I've written a proof of the following lemma,
lemma add_one_le_exp (x:ℝ) : x + 1 ≤ real.exp x
which resolves the following TODO: https://github.com/leanprover-community/mathlib/blob/master/src/data/complex/exponential.lean#L1140
I would be happy to submit this in a PR. My github user is isadofschi

[Johan Commelin]

@Iván Sadofschi Costa Welcome! See https://github.com/leanprover-community/mathlib/invitations.