2) I have locally generated list l1 and H1 related to this

```
H1: count_occ Nat.eq_dec
match l1 with
| [] => []
| c :: t => c :: firstn m t
end (S z) <=
count_occ Nat.eq_dec
match l1 with
| [] => []
| c :: t => c :: firstn m t
end 0
```

z m c are nat. l1 is list nat.

2) I have an expression , then it it would be equal to below one (by using l1 from H1)

```
(b :: firstn m l1)
(b :: firstn m (c :: firstn m t))
(b ::c::firstn m t)
```

3) Above can be helpful in proving

```
count_occ Nat.eq_dec (k1::firstn m l1) (S z) <= count_occ Nat.eq_dec (k1 :: firstn m l1) 0
```

k1 is nat.

Last updated: Oct 01 2023 at 18:01 UTC