[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

jerome