:: deftheorem Def1 defines SDMinDigit RADIX_5:def 1 :
for i, m, k being Nat st k >= 2 holds
( ( 1 <= i & i < m implies SDMinDigit (m,k,i) = (- (Radix k)) + 1 ) & ( ( not 1 <= i or not i < m ) implies SDMinDigit (m,k,i) = 0 ) );