Soundness of powMonotone2

[alejandrorusso]

The axiom

powMonotone2 :: forall a b c . (b <= c) :- ( (a^b) <= (a ^c))

is not true when a is 0, and b is 0 and c is any positive number.

For instance, a = 0, b = 0, c = 1, then we have

(0 <= 1) :- (0^0 <= 0^1)

which is

(0 <= 1) :- (1 <= 0)

One way to solve this is asking a to be a positive number

powMonotone2 :: forall a b c . (0 < a, b <= c) :- ( (a^b) <= (a ^c))

or

powMonotone2 :: forall a b c . (1 <=a , b <= c) :- ( (a^b) <= (a ^c))

if a is thought to be of kind Nat.

[RyanGlScott]

I'm in favor of fixing this by adding a 1 <= a constraint.