:: deftheorem defines divides NAT_D:def 3 :
for k, l being natural Number holds
( k divides l iff ex t being Nat st l = k * t );