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

Re: [PVS-Help] GCD divides



On Thu, Aug 28, 2008 at 6:49 PM, Jerome <jerome@xxxxxxxxxxxxxx> wrote:
> 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

Since gcd_divides tells you that gcd(y, z) divides both y and z, you
have divides(x, gcd(y, z)) AND divides(gcd(y, z), y).  Then
divides_transitive from the prelude gives you what you want.
-- 
Jerry James
http://loganjerry.googlepages.com/