for n being Nat holds indexp n <= n