H: count_occ l (S a) <= count_occ l 0 goal: count_occ (0::l) (S a) <= count_occ(0::l) 0 .
I am solving it by lia but it is not solving. What tactic i should apply?
Did you try simplor cbn before lia?
simpl
cbn
lia
Last updated: Sep 30 2023 at 05:01 UTC