Различить цель в Coq

Question

У меня есть два условия для чисел нац:

H:  a < b
H1: b < a

Как различить цель? Существует ли какая-либо тактика для <? </p>

Answer 1

Использование lia:

From Coq Require Import Lia.

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

Подробнее о lia и других процедурах принятия решений по арифметике c можно узнать здесь .

Answer 2

Для справки, ручное доказательство не так сложно в этом случае:

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma foo a b (a_lt_b : a < b) : b < a -> False.
Proof. by rewrite ltnNge (ltnW a_lt_b). Qed.