a,b,y,n:
. GCD(a;b;y) 
GCD(n
a;nb;ny)a,b:. a | b (n:. na | nb)a,b,y1,y2:. GCD(a;b;y1) GCD(a;b;y2) (y1 ~ y2)a,b:. 
u,v:. GCD(a;b;ua+vb)a,b,c:. a | b a | bca,b1,b2:. a | b1 a | b2 a | b1+b2| Rank | Theorem | Name |
| 4 | a,b,y,n:. GCD(a;b;y) GCD(na;nb;ny) | [gcd_p_mul] |
| cites the following: | ||
| 0 | a,b:. a | b (n:. na | nb) | [divides_mul] |
| 0 | a,b,y1,y2:. GCD(a;b;y1) GCD(a;b;y2) (y1 ~ y2) | [gcd_unique] |
| 3 | a,b:. u,v:. GCD(a;b;ua+vb) | [bezout_ident] |
| 0 | a,b,c:. a | b a | bc | [divisor_of_mul] |
| 0 | a,b1,b2:. a | b1 a | b2 a | b1+b2 | [divisor_of_sum] |