Should poweR return 0 if the exponent is negative?

[jmmarulang]

See the following definition

analysis/theories/exp.v

Lines 996 to 1001 in 97d0779

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

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 )