FDL > PVS > Number Theory > gcd > gcd is max > pf:gcd is max > 1 > 1 > 2 > 1 (4 nodes)

Conclusion

-1. (i!1 /= 0) OR (j!1 /= 0)
-2. divides(kk!1, i!1)
-3. divides(kk!1, j!1)

1. EXISTS UB : FORALL y:({k:posnat | divides(k, i!1) AND divides(k, j!1)}) : y < = UB
2. kk!1 < = max({k:posnat | divides(k, i!1) AND divides(k, j!1)})