for i, k being Nat st i + 1 <= k holds
1 <= k -' i