In Coq how I can write this statement" Z(nat) number of elements are not member of list"?

I'm not sure I see you right. But for the first approximation I would do something like

```
From Coq Require Import List.
Import ListNotations.
Fixpoint eqb_nat (a b : nat) : bool :=
match a, b with
| O, O => true
| S a', S b' => eqb_nat a' b'
| _, _ => false
end.
Fixpoint InLst (lst : list nat) (x : nat) : bool :=
match lst with
| [] => false
| x'::xs' => if eqb_nat x x' then true else InLst xs' x
end.
Fixpoint Z (all lst: list nat) : nat :=
match all with
| [] => 0
| x::xs => let nx := if InLst lst x then 1 else 0 in nx + Z xs lst
end.
```

so, `all`

is a list of all possible elements.

Last updated: Jun 20 2024 at 11:02 UTC