a,b:
. GCD(a;0;b) 
a = b 
a = -ba:. a | ab:. b | 0a,b:. a | b b | a a = 
b| Rank | Theorem | Name |
| 4 | a,b:. GCD(a;0;b) a = b a = -b | [gcd_p_zero_rel] |
| cites the following: | ||
| 0 | a:. a | a | [divides_reflexivity] |
| 0 | b:. b | 0 | [any_divs_zero] |
| 3 | a,b:. a | b b | a a = b | [divides_anti_sym] |