coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Contradicting Zneg p >= 2

From: frank maltman <frank.maltman AT googlemail.com>
To: <coq-club AT inria.fr>
Subject: [Coq-Club] Contradicting Zneg p >= 2
Date: Wed, 8 Jun 2011 11:33:09 +0000
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=date:from:to:subject:message-id:x-mailer:mime-version:content-type :content-transfer-encoding; b=kZqztzTqE2D8REzUdI7j6217/Zb6RWPDGzQciEB3FfnoZ6Om2HO3hvcnpMk23ZCozS OR7qKADrkc7nIw4PKEQf6Ke/uHDZAW8oM+EIX2KxtFRIwQ6eAd3xmHWh8kixGgCUG0aS 5DqOZiWbqoUqhEuS44j4UWUMBHdN4X5TFiDBM=

Hello.

Given:

  p : positive
  HM : Zneg p >= 2
  ============================
   0 < 0

I have a proof of Zneg p < 2:

> Check (Zlt_le_trans (Zneg p) 0 2 (Zlt_neg_0 p) (Zlt_le_weak 0 2 (Zgt_lt 2 0
> (Zgt_pos_0 2)))).
Zlt_le_trans (Zneg p) 0 2 (Zlt_neg_0 p)
  (Zlt_le_weak 0 2 (Zgt_lt 2 0 (Zgt_pos_0 2)))
     : Zneg p < 2

According to the manual, I use the 'contradict' tactic to show that
the context contains an inconsistent hypothesis:

  p : positive
  ============================
   ~ Zneg p >= 2

How do I get from a proof of 'Zneg p < 2' to a proof of '~ Zneg p >= 2'?

There seem to be various lemmas in Coq.ZArith.Zorder but I'm looking for
something matching:

  forall m n : Z, m < n -> ~ m >= n.

... and can't find it (seems to have just about every other combination
but that one).

[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