for n being Nat st n > 1 holds
Euler n <= n - 1