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: Oct 13 2024 at 01:02 UTC