H1: a>0

H2: a=0 (while a is natural number). I am unable to solve it by lia. What could be the reason?

what's the error message?

This works :

```
Require Import Lia.
Goal forall a, a>0 -> a=0 -> False.
intros H1 H2.
now lia.
Qed.
```

Directly apply lia. Not written in this way Goal forall a, a>0 -> a=0 -> False. Whats the difference between these ways?

(deleted)

```
@**pianke**
```

This was an answer to a part of of your previous post you moved later to another topic.

You may use the `inversion`

tactic:

```
Require Import List Arith Lia.
Import ListNotations.
Goal forall (A:Type) (x: A), In x [] -> False.
Proof.
intros A x H. inversion H.
Qed.
Goal forall (A:Type) (x y:A) l, In x (y::l) -> x = y \/ In x l.
Proof.
intros A x y l H. inversion H.
- left; congruence.
- now right.
Qed.
```

Last updated: Jun 24 2024 at 13:02 UTC