theorem Th37: :: NUMBER16:37
for a, b, n being Nat st 0 < a & a < b & b <= n holds
a * b divides n !