`ln_eq0`

[affeldt-aist]

analysis/theories/exp.v

Line 1247 in 6600f40

Lemma lne_eq0 x : (lne x == 0) = (x == 1).

we maybe need the analogous lemma for real numbers

@garrigue @gregweng