[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
>> 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