a,b,y,k:
. GCD(a;b;y) 
GCD(a;b+k
a;y)a,b:. ab = baa,b1,b2:. a | b1 a | b2 a | b1+b2a,b,c:. a | b a | bc| Theorem | Name |
| a,b,y,k:. GCD(a;b;y) GCD(a;b+ka;y) | [gcd_p_shift] |
| cites the following: | |
| a,b:. ab = ba | [mul_com] |
| a,b1,b2:. a | b1 a | b2 a | b1+b2 | [divisor_of_sum] |
| a,b,c:. a | b a | bc | [divisor_of_mul] |