The Coq mailing list

["Balazs Vegvari" <balazs.vegvari AT gmail.com>]

one thing came into my mind after reading documentation of the omega
tactic: what if omega could not solve a similar system, for example
adding a nonlinear product to the example? How would I prove this
manually in that case?

thanks,
Balazs

On Thu, Aug 28, 2008 at 7:17 AM, Balazs Vegvari
<balazs.vegvari AT gmail.com>
 wrote:
> Hi Adam,
>
> It worked, I really have to learn a lot.
>
>
> thanks,
> Balazs
>
> On Thu, Aug 28, 2008 at 12:06 AM, Adam Chlipala 
>Â <adamc AT hcoop.net>
>  wrote:
>> Balazs Vegvari wrote:
>>>
>>> I am just learning coq and I don't kow how to prove this:
>>>
>>> forall x y : Z, x <= y + 1 -> x <= y \/ x = y + 1
>>>
>>> Any suggestion is welcome.
>>>
>>
>> Did you have a particular constraint on the proof technique in mind?  Your
>> theorem statement falls into the theory of "quantifier-free linear
>> arithmetic," which is one of the most widely-used decidable theories.  The
>> [omega] tactic solves it instantly (after [intros]).
>>
>