let m, n be Nat; :: thesis: ( m <= n implies m ! divides n ! )
defpred S₁[ Nat] means ( m <= $1 implies m ! divides $1 ! );
A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
assume m <= k + 1 ; :: thesis: m ! divides (k + 1) !

per cases then ( m <= k or m = k + 1 ) by NAT_1:8;

suppose A4: m <= k ; :: thesis: m ! divides (k + 1) !

A5: (k + 1) ! = (k !) * (k + 1) by NEWTON:15;
1 divides k + 1 by INT_2:12;
then (m !) * 1 divides (k + 1) ! by A3, A4, A5, NAT_3:1;
hence m ! divides (k + 1) ! ; :: thesis: verum

end;

suppose m = k + 1 ; :: thesis: m ! divides (k + 1) !

hence m ! divides (k + 1) ! ; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence ( m <= n implies m ! divides n ! ) ; :: thesis: verum