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].
I don't understand which lemma you want to prove.
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.
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?
May be 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