theorem MDF1: :: NEWTON07:6

for n, k being Nat holds (min (n,k)) ! divides n !