test-suite/micromega/bug_12210.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

Require Import PeanoNat Lia.

Goal forall x, Nat.le x x.
Proof.
intros.
lia.
Qed.

Goal forall x, Nat.lt x x -> False.
Proof.
intros.
lia.
Qed.

Goal forall x, Nat.eq x x.
Proof.
intros.
lia.
Qed.