proposition: Lemma count_count_occ {l n} : count (l : list nat) (n : nat) = count_occ PeanoNat.Nat.eq_dec l n.
proof: Proof. induction l as [|a l IH]; [reflexivity|]. cbn. destruct (PeanoNat.Nat.eq_dec a n) as [->|Han%PeanoNat.Nat.eqb_neq]. - now rewrite PeanoNat.Nat.eqb_refl, IH. - now rewrite PeanoNat.Nat.eqb_sym, Han. Qed.
imports: List Lia