0
$\begingroup$

According to the documentation, there should be a Lemma le_not_gt_iff in Coq.Structures.OrdersFacts, but I haven't succeeded in referencing it.

I am trying to prove 2 < 1 → False as part of a proof. I tried Nat.order tactic but it didn't work.

So now I am looking into Coq.Structures.OrdersFacts to find another Lemma that can help, and found le_not_gt_iff.

The problem I have is that the import

Require Import Coq.Structures.OrdersFacts.

doesn't seem to be enough to have access to the Lemma. I see it seems to be encapsulated in a module definition OrderedTypeFullFacts, but I don't know how to import that.

Improve this question
New contributor
kutschkem is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

Unless there are educational reasons for not using it, I would use the lia tactic:

Require Import Lia.
Goal  2 < 1 -> False.
lia.
Improve this answer
New contributor
M Soegtrop is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
$\endgroup$
2
  • $\begingroup$ Perfect, that worked. There is no educational reason, I am just a beginner that didn't know lia existed. $\endgroup$
    – kutschkem
    Commented Jul 3 at 8:41
  • $\begingroup$ You will like lia - as long as you don't multiply variables (lia is for "linear integer arithmetic" - multiplication with constants is fine) it can solve most complicated networks of equalities, inequalities and a bit of logic. $\endgroup$
    – M Soegtrop
    Commented Jul 3 at 8:44

Not the answer you're looking for? Browse other questions tagged or ask your own question.