:: deftheorem defines #divs NUMBER18:def 3 :
for n being Nat holds #divs n = sigma (0,n);