I'm working on the definition of real numbers from “Real Analysis: A Constructive Approach” by Mark Bridger. Several examples require to prove that powers and roots are monotonic.
I proved $\forall n\geq 1\, \forall a>0\, \forall b>0\, (a^n\leq b^n\to a\leq b)$ from $\forall n\geq 1\, \forall a>0\, \forall b>0\, (a<b\to a^n<b^n)$ using the definition $a\leq b := \lnot a>b$.
I don't know how to prove $\forall n\geq 1\, \forall a>0\, \forall b>0\, (a^n<b^n\to a<b)$. Is it even possible without going down to rational intervals?
As algebraically $$ b^n-a^n=(b-a)(a^{n-1}+a^{n-2}b+a^{n-3}b^2+…+b^{n-1}) $$ and with $a,b$ positive the second factor on the right is also positive, $b^n-a^n$ and $b-a$ will always have the same sign.