proposition: Theorem count_occ_In l x : In x l <-> count_occ l x > 0.
proof: Proof. induction l as [|y l IHl]; simpl. - split; [destruct 1 | apply Nat.nlt_0_r]. - destruct eq_dec as [->|Hneq]; rewrite IHl; intuition (apply Nat.lt_0_succ). Qed.
imports: PeanoNat