FDL > PVS > Number Theory > gcd > gcd is max > pf:gcd_is_max : proof (11 nodes)

Conclusion

1. FORALL i:int, j:int, kk:nzint : (((i /= 0) OR (j /= 0)) AND divides(kk, i) AND divides(kk, j)) IMPLIES (kk < = gcd(i, j))