FDL > PVS > Number Theory > gcd > gcd TCC1 > pf:gcd TCC1 > 1 > 1 > 1

Conclusion

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