Should poweR return 0 if the exponent is negative?

[jmmarulang]

See the following definition

https://github.com/math-comp/analysis/blob/97d07798ab1fd1889ed707181c06cf98c438e408/theories/exp.v#L996-L1001

Note that for real numbers, the limit of the power function when the exponent is negative, goes to 0.

[hoheinzollern]

So the proposed alternative definition could be:

 Definition poweR x r := 
   match x with 
   | x'%:E => (x' `^ r)%:E 
   | +oo => if r == 0%R then 1%E else if r > 0 then +oo else 0%E
   | -oo => 1%E
   end. 

(edited after discussion with @jmmarulang )