z:
. (z | a) & (z | b) 
(z | y))a,b,y:. GCD(a;b;y) 
Prop
c:. a = b
ca,b:. (a | b) Prop| Who Cites gcd p? | |
| gcd_p | Def GCD(a;b;y) == (y | a) & (y | b) & (z:. (z | a) & (z | b) (z | y)) |
| Thm* a,b,y:. GCD(a;b;y) Prop | |
| divides | Def b | a == c:. a = bc |
| Thm* a,b:. (a | b) Prop |
| Syntax: | GCD(a;b;y) | has structure: | gcd_p(a; b; y) |
About:
 |  |  |  |  |  |  |  |  |  |