What are the existing well-founded orders provided for integers (type Z) in the Coq library? Use them to define a function that coincides with the factorial function on positive integers and returns zero for other integers.