Define the factorial function on integers (with the value zero for negative arguments) by using this method and the well-founded relation Zwf.