AH
Once we write this down, F* automatically proves that factorial satisfies all these properties.
The factorial function is, however, a total function on non-negative integers. We can ask F* to check that this is indeed the case by writing:
val factorial: x:int{x>=0} -> Tot int