:: deftheorem defines GBP SCMP_GCD:def 2 :
GBP = intpos 0;