PoweR with extended real exponents

[jmmarulang]

Motivation for this change

Checklist

• [ ] added corresponding entries in CHANGELOG_UNRELEASED.md

• [ ] added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

Maybe you shouldn't remove ln_eq0 and change the proof of lne_eq0.

[jmmarulang]

I will give it a try.

[jmmarulang]

Unrelated to that. Im starting to think that lne returning -oo instead of 0 for negative numbers is more cumbersome than beneficial. Specially when trying to work with poweR you are forced to deal with a lot more cases, since it is no longer true that (x < 0) -> x ^ y = 1`.

[hoheinzollern]

@affeldt-aist, after discussing this development with @jmmarulang, we think that this new definition of the power function is more cumbersome to work with than the one proposed in #1613, we should discuss whether it's a good idea to polish the current version or find another approach.