proposition: Lemma count_pos_of_mem : forall x P l, mem x l -> P x -> count P l > 0.
proof: Proof. Proof using. introv. rewrite* count_pos_eq_exists_mem. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)