## Stream: Coq users

### Topic: Nat counting

#### zohaze (May 21 2022 at 05:14):

I have list of natural numbers , want to extract list information from below .Please guide me how to write it(in form of lemma).
count_occ Nat.eq_dec [2,4,2,8] 2 > count_occ Nat.eq_dec [2,4,2,8] 8 ->
l= [2,4,2,8].

#### Pierre Castéran (May 21 2022 at 07:10):

I don't understand which lemma you want to prove.

• There is no information about the variable `l`
• The left hand side of your implication `count_occ Nat.eq_dec [2;4;2;8] 2 > count_occ Nat.eq_dec [2;4;2;8] 8 ` reduces to `2 > 1` (just try `cbn`)
thus is trivially provable.

• Please note also that there were syntax errors (list notations) in your question.

#### zohaze (May 21 2022 at 15:59):

cbn works .Thanks.

#### pianke (Jun 20 2022 at 13:30):

l is non empty list of nat.
H: count_occ Nat.eq_dec l 2 > count_occ Nat.eq_dec l 8
Goal: count_occ Nat.eq_dec (2::l ) 2 > count_occ Nat.eq_dec (2::l) 8. lia should solve it but it is not working .How to prove it?

#### Pierre Castéran (Jun 20 2022 at 14:31):

May be `lia` did not find `H`. You may reintroduce it in the current goal.
`generalize H. cbn. lia. ` works.

Last updated: Oct 03 2023 at 04:02 UTC