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