Stream: Coq users

Topic: Number of elements

view this post on Zulip pianke (Jun 04 2022 at 04:13):

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?

view this post on Zulip Pierre Castéran (Jun 04 2022 at 05:42):

Did you try simplor cbn before lia?

Last updated: Apr 20 2024 at 07:01 UTC