let n be Nat; :: thesis: ( n > 1 implies (n + 2) ! > (n !) + 2 )
assume A1: n > 1 ; :: thesis: (n + 2) ! > (n !) + 2
then A2: n + 1 > 1 + 1 by XREAL_1:8;
then A3: n + 1 > 1 by XXREAL_0:2;
n ! >= n by NEWTON:38;
then A4: n ! > 1 by XXREAL_0:2, A1;
n + 1 <= (n + 1) + 1 by NAT_1:11;
then A5: (n + 1) ! <= (n + 2) ! by ASYMPT_1:56;
(n + 1) ! <> (n + 2) !

proof

assume (n + 1) ! = (n + 2) ! ; :: thesis: contradiction
then ((n + 1) !) * 1 = ((n + 1) !) * ((n + 1) + 1) by NEWTON:15;
then 1 = (n + 1) + 1 by XCMPLX_1:5;
then 0 = n + 1 ;
hence contradiction ; :: thesis: verum

end;

then A6: (n + 1) ! < (n + 2) ! by XXREAL_0:1, A5;
(n + 1) ! = (n + 1) * (n !) by NEWTON:15;
then A7: (n + 1) ! >= (n + 1) + (n !) by A3, Th1, A4;
(n + 1) + (n !) > (n !) + 2 by XREAL_1:8, A2;
then (n + 1) ! >= (n !) + 2 by A7, XXREAL_0:2;
hence (n + 2) ! > (n !) + 2 by A6, XXREAL_0:2; :: thesis: verum