coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Contradicting Zneg p >= 2

From: frank maltman <frank.maltman AT googlemail.com>
To: Evgeny Makarov <emakarov AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Contradicting Zneg p >= 2
Date: Wed, 8 Jun 2011 12:32:52 +0000
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=date:from:to:cc:subject:message-id:in-reply-to:references:x-mailer :mime-version:content-type:content-transfer-encoding; b=STisfB8a5CRnNT6q/2BbnJhtHOcaXKXBP5mGzY+573B+ovU/+gEDuuiXYK18dZV8Ht l+3BkCarItzVnPGmbyQt1q3vBpmRtnKyLUDFX1sU3octR4VeSSidq6yNXhZu1ZUPuj/0 EFkb69kTv91RcEPGCwW6/S5enN1q1JkVRGiM0=

On Wed, 8 Jun 2011 14:09:21 +0200
Evgeny Makarov
<emakarov AT gmail.com>
wrote:

> Hi, Frank,
>
> Yes, searching in the library for exact match can be frustrating.
>
> Suppose we start with
>
> Goal forall m n : Z, m < n -> ~ m >= n.
> intros m n H H1.
>
> There are several ways to finish the proof.

Thank you!

Of course, of all the tactics I should have tried first, I somehow
failed to try 'auto'.

  p : positive
  ============================
   Zneg p >= 2 -> False

> auto.
Proof completed.

*ahem*

[Coq-Club] Contradicting Zneg p >= 2, frank maltman
- Re: [Coq-Club] Contradicting Zneg p >= 2, Evgeny Makarov
  - Re: [Coq-Club] Contradicting Zneg p >= 2, frank maltman