```
From mathcomp Require Import all_ssreflect zify .
Lemma foo {A: eqType}: forall (x: A) (l: list A), (x \in l -> False) -> x \notin l.
Proof.
move => x l x_not_in_l.
apply: negbT. (* x \in l = false*)
(* stuck here*)
```

I am not even sure if `negbT`

is the right approach , I searched for `\notin`

and `ctrl+f`

ed for reflect but didn't find anything useful.

```
Locate "\notin".
```

gives

```
Notation "x \notin A" := (negb (in_mem x (mem A))) : bool_scope (default interpretation)
```

and

```
Locate "\in"
```

gives

```
Notation "x \in A" := (in_mem x (mem A)) : bool_scope (default interpretation)
```

so `\notin`

is just the boolean negation (`negb`

) of `\in`

and anything on negation (like `negP`

for instance) should work.

negP was the thing i was struggling to find, thanks!

walker has marked this topic as resolved.

Last updated: Jul 15 2024 at 21:02 UTC