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 ->
I don't understand which lemma you want to prove.
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
thus is trivially provable.
Please note also that there were syntax errors (list notations) in your question.
cbn works .Thanks.
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?
lia did not find
H. You may reintroduce it in the current goal.
generalize H. cbn. lia. works.
Last updated: Jan 29 2023 at 06:02 UTC