theorem Th45: :: NUMBER08:45

for n being non zero Nat holds Euler_factorization_2 n <= n - 1