proposition: Lemma count_occ_elt_neq l1 l2 x y : x <> y -> count_occ (l1 ++ x :: l2) y = count_occ (l1 ++ l2) y.
proof: Proof. intros Hxy. rewrite ? count_occ_app; cbn. now destruct (eq_dec x y) as [Heq | Hneq]; [ contradiction Hxy | ]. Qed.
imports: PeanoNat