[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] GCD divides

This is another one of those, "can the prelude help me out" questions:
I'm trying to prove the following:

   FORALL (x, y, z: posnat):
     divides(x, gcd(y, z)) IMPLIES divides(x, y)

Can anyone think of something in the prelude that would help me
along. I've checked most of the theorems in ints, but haven't found
anything useful. Thanks