Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant