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

Conclusion

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

1. kk!1 < = gcd(i!1, j!1)

Tactic
 EXPAND "gcd"
Premise 1.   (has proof of 9 steps)

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

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