Re: [PVS-Help] GCD divides

[Jerome <jerome@xxxxxxxxxxxxxx>]

Thanks, Jerry. That did the trick.

jerome

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
>http://loganjerry.googlepages.com/
>