proposition: Lemma count_pos_eq_exists_mem : forall P l, (count P l > 0) = (exists x, mem x l /\ P x).
proof: Proof. Proof using. intros. rewrite <- LibList.count_pos_eq_exists_mem. unfold count. rewrite abs_nonneg; math. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)