Want to count two natural numbers(k1 and k2)that exist in the list. On the basis of this count I want to to find greater element.(count k1 l < count k2 l).

I have (a::l0) list nat. There is function f, whose input is (c::l0) and output is l1. During recursive call number of elements

in l1 are going to increase.( m ,c,c0 & k are nat).

```
H: (m > 0 ->
count_occ Nat.eq_dec (firstn m 11) 0 <= count_occ Nat.eq_dec (firstn m 11) (S k) ->
count_occ Nat.eq_dec (firstn (S m) l1 0 <= count_occ Nat.eq_dec (firstn (S m) l1 (S k)))).
```

When (c::c0::l0) is given to function f, then

```
Goal: count_occ Nat.eq_dec (firstn (S m) l1 0 <= count_occ Nat.eq_dec (firstn (S m) l1 (S k).
```

To prove above i should focuss on role of c0 in f? How to proceed? I have already asked but might be not properly asked.

Last updated: Feb 01 2023 at 13:03 UTC