:: deftheorem defines intpos SCMP_GCD:def 1 :
for k being Nat holds intpos k = dl. k;