for n, b being Nat st b > 1 holds
( b divides n iff (digits (n,b)) . 0 = 0 )