coq - How to simplify counting relation between natural numbers

Question

I want to prove the following lemma. I am calling two functions, one is (f_value) defined below.Second one is l_count - it requires two input arguments (nat &list nat)and one nat as output.It counts number of elements in the list that are less than input argument(nat). f_value gives zero when input nat(check)is zero and some non zero term in another case.I want to ask under what condition output value of f_value is zero when input nat(check) is not zero.check is largest element of list.For example 4[4] in this case check(4 )is not zero and f_value is zero,4[4,4,4].

Fixpoint f_value (check: nat) (l: list nat) : nat :=
match check with
| O => 0
| S a' => (l_count check l) + (f_value a' l)
end.

Theorem f_value_0:forall(n p:nat)(l:list nat),
 length l =? 0 = false ->
 (0 = f_value ((S n) l + S p)l).  

Answer 1

等待大神答复