let n, k be Nat; :: thesis: ( k >= 2 * n implies 2 |^ n divides k ! )
assume k >= 2 * n ; :: thesis: 2 |^ n divides k !
then min (k,(2 * n)) = 2 * n by XXREAL_0:def 9;
then A1: (2 * n) ! divides k ! by MDF1;
(2 !) |^ n divides (2 * n) ! by FPD;
hence 2 |^ n divides k ! by A1, INT_2:9; :: thesis: verum