Certain famous combinatorial sequences, such as the Catalan numbers and the Motzkin numbers, when taken modulo a prime power, can be computed by finite automata. Many theorems about such sequences can therefore be proved using Walnut, which is an implementation of a decision procedure for proving various properties of automatic sequences. In this paper we explore some results (old and new) that can be proved using this method.