coqcoq-tacticcoqide

Discriminate goal in Coq

I have two conditions for nat numbers:

H:  a < b
H1: b < a

How to discriminate goal? Does exist any tactics for < ?

Solution

  • Use lia:

    From Coq Require Import Lia.

Goal forall a b, a < b -> b < a -> False.
  lia.
Qed.

    You can learn more about lia and other decision procedures for arithmetic here.