theorem :: SCMP_GCD:9

for n being Nat holds
( n < 15 iff n in dom GCD-Algorithm ) by Th8, AFINSQ_1:66;