[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] GCD divides
Thanks, Jerry. That did the trick.
On Thu, Aug 28, 2008 at 09:49:49PM -0600, Jerry James wrote:
>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
>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.