let x be Divisor of n; :: thesis: x is n _or_smaller

consider k being Integer such that

A1: x * k = n by Def2, INT_1:def 3;

k >= 0 by A1;

then reconsider k = k as Element of NAT by INT_1:3;

k <> 0 by A1;

hence x is n _or_smaller by A1, NAT_1:24; :: thesis: verum

consider k being Integer such that

A1: x * k = n by Def2, INT_1:def 3;

k >= 0 by A1;

then reconsider k = k as Element of NAT by INT_1:3;

k <> 0 by A1;

hence x is n _or_smaller by A1, NAT_1:24; :: thesis: verum