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

gcd_divides: LEMMA ((i /= 0) OR (j /= 0)) IMPLIES (divides(gcd(i, j), i) AND divides(gcd(i, j), j))

Subproof Addresses (10 steps)
top :
top 1 :
top 1 1 :
top 1 1 1 :
top 1 1 2 :
top 1 1 2 1 :
top 1 1 2 1 1 :
top 1 1 2 1 2 :
top 1 1 2 1 3 :
top 1 1 2 1 4 :