Description: Stirling's approximation formula for n factorial. The proof follows
two major steps: first it is proven that S and n factorial are
asymptotically equivalent, up to an unknown constant. Then, using
Wallis' formula for π it is proven that the unknown constant is the
square root of π and then the exact Stirling's formula is
established. This is Metamath 100 proof #90. (Contributed by Glauco
Siliprandi, 29-Jun-2017)