factorial is positive also for n=0

Thus, if a variable is known to be a nonnegative integer, its factorial should be known to be positive.
Again, see #8500.