FDL > PVS > Number Theory > gcd > gcd_is_max : formula-decl

gcd_is_max: LEMMA (((i /= 0) OR (j /= 0)) AND divides(kk, i) AND divides(kk, j)) IMPLIES (kk < = gcd(i, j))

Subproof Addresses (11 steps)
top :
top 1 :
top 1 1 :
top 1 1 1 :
top 1 1 1 1 :
top 1 1 1 2 :
top 1 1 2 :
top 1 1 2 1 :
top 1 1 2 1 1 :
top 1 1 2 1 1 1 :
top 1 1 2 1 1 1 1 :