proposition: Lemma count_occ_rev l x : count_occ eq_dec (rev l) x = count_occ eq_dec l x.
proof: Proof. induction l as [|a l IHl]; trivial. cbn; rewrite count_occ_app, IHl; cbn. destruct (eq_dec a x); rewrite Nat.add_comm; reflexivity. Qed.
imports: PeanoNat