theorem :: RADIX_2:1

for a being Nat holds a mod 1 = 0