https://github.com/math-comp/analysis/blob/6600f40c3ab9d8e342f1991e889599b1528a0255/theories/exp.v#L1247 we maybe need the analogous lemma for real numbers @garrigue @gregweng
