set g = seq_n^ 1;
let f be Real_Sequence; :: thesis:
assume A1: for n being Element of NAT holds f . n = Step1 n ; :: thesis:
f is eventually-positive

proof

take 1 ; :: according to ASYMPT_0:def 6 :: thesis:
let n be Element of NAT ; :: thesis:
assume n >= 1 ; :: thesis:
then A2: ex m being Element of NAT st
( m ! <= n & n < (m + 1) ! & Step1 n = m ! ) by Def9;
f . n = Step1 n by A1;
hence not f . n <= 0 by A2, NEWTON:23; :: thesis:

end;

then reconsider f = f as eventually-positive Real_Sequence ;

now

let k be Element of NAT ; :: thesis:
thus f . k <= f . (k + 1) :: thesis:

proof

per cases ;

suppose A3: k = 0 ; :: thesis:

A4: f . (0 + 1) = Step1 1 by A1;
f . 0 = Step1 0 by A1
.= 0 by Def9 ;
hence f . k <= f . (k + 1) by A3, A4; :: thesis:

end;

suppose k > 0 ; :: thesis:

then consider n1 being Element of NAT such that
A5: n1 ! <= k and
A6: k < (n1 + 1) ! and
A7: Step1 k = n1 ! by Def9;
A8: k + 1 <= (n1 + 1) ! by A6, INT_1:20;
A9: k <= k + 1 by NAT_1:11;
A10: f . k = n1 ! by A1, A7;

per cases by A8, XXREAL_0:1;

suppose A11: k + 1 < (n1 + 1) ! ; :: thesis:

n1 ! <= k + 1 by A9, A5, XXREAL_0:2;
then Step1 (k + 1) = n1 ! by A11, Def9;
hence f . k <= f . (k + 1) by A1, A10; :: thesis:

end;

suppose A12: k + 1 = (n1 + 1) ! ; :: thesis:

A13: (n1 + 1) ! > 0 by NEWTON:23;
n1 + 2 > 0 + 1 by XREAL_1:10;
then 1 * ((n1 + 1) ! ) < (n1 + 2) * ((n1 + 1) ! ) by A13, XREAL_1:70;
then A14: k + 1 < ((n1 + 1) + 1) ! by A12, NEWTON:21;
f . (k + 1) = Step1 (k + 1) by A1
.= (n1 + 1) ! by A12, A14, Def9 ;
hence f . k <= f . (k + 1) by A10, Lm51, NAT_1:11; :: thesis:

end;

then A15: for k being Element of NAT st k >= 0 holds
f . k <= f . (k + 1) ;
A16: 1 = 2 - 1 ;

A17: now

set h = f taken_every 2;
assume f is smooth ; :: thesis:
then f is_smooth_wrt 2 by ASYMPT_0:def 20;
then f taken_every 2 in Big_Oh f by ASYMPT_0:def 19;
then consider t being Element of Funcs NAT ,REAL such that
A18: t = f taken_every 2 and
A19: ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) ;
consider c being Real, N being Element of NAT such that
c > 0 and
A20: for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) by A19;
set n2 = max (max N,3),([/c\] + 1);
A21: max (max N,3),([/c\] + 1) >= max N,3 by XXREAL_0:25;
max N,3 >= N by XXREAL_0:25;
then A22: max (max N,3),([/c\] + 1) >= N by A21, XXREAL_0:2;
A23: max (max N,3),([/c\] + 1) >= [/c\] + 1 by XXREAL_0:25;
A24: max (max N,3),([/c\] + 1) is Integer by XXREAL_0:16;
A25: max N,3 >= 3 by XXREAL_0:25;
then A26: max (max N,3),([/c\] + 1) >= 3 by A21, XXREAL_0:2;
reconsider n2 = max (max N,3),([/c\] + 1) as Element of NAT by A21, A24, INT_1:16;
set n1 = (n2 ! ) - 1;
A27: n2 > 2 by A26, XXREAL_0:2;
then A28: n2 ! >= 2 by Lm51, NEWTON:20;
then A29: (n2 ! ) - 1 >= 1 by A16, XREAL_1:11;
set n3 = n2 - 1;
1 + 1 <= n2 by A26, XXREAL_0:2;
then A30: 1 <= n2 - 1 by XREAL_1:21;
A31: n2 - 1 >= 1 by A16, A27, XREAL_1:11;
reconsider n1 = (n2 ! ) - 1 as Element of NAT by A29, INT_1:16;
A32: t . n1 = f . (2 * n1) by A18, ASYMPT_0:def 18;
n2 ! > n2 by A26, Lm53;
then n2 ! >= n2 + 1 by INT_1:20;
then n1 >= n2 by XREAL_1:21;
then n1 >= N by A22, XXREAL_0:2;
then A33: t . n1 <= c * (f . n1) by A20;
n2 < n2 + 1 by NAT_1:13;
then n2 * (n2 ! ) < (n2 + 1) * (n2 ! ) by A28, XREAL_1:70;
then A34: n2 * (n2 ! ) < (n2 + 1) ! by NEWTON:21;
(n2 ! ) + 2 <= (n2 ! ) + (n2 ! ) by A28, XREAL_1:8;
then A35: n2 ! <= (2 * (n2 ! )) - (2 * 1) by XREAL_1:21;
A36: (n2 ! ) - 1 < (n2 ! ) - 0 by XREAL_1:17;
then A37: 2 * n1 < 2 * (n2 ! ) by XREAL_1:70;
reconsider n3 = n2 - 1 as Element of NAT by A31, INT_1:16;
n3 ! >= 1 by A31, Lm51, NEWTON:19;
then 1 * 1 <= (n2 - 1) * (n3 ! ) by A30, Lm20;
then n2 * 1 <= ((n2 - 1) * (n3 ! )) * n2 by XREAL_1:66;
then n2 <= (n2 - 1) * ((n3 ! ) * (n3 + 1)) ;
then n2 <= (n2 - 1) * (n2 ! ) by NEWTON:21;
then A38: (n2 ! ) + n2 <= ((n2 ! ) * 1) + ((n2 - 1) * (n2 ! )) by XREAL_1:8;
A39: n3 + 1 = n2 + 0 ;
then n2 * (n3 ! ) = n2 ! by NEWTON:21;
then n2 * (n3 ! ) <= (n2 * (n2 ! )) - n2 by A38, XREAL_1:21;
then n3 ! <= (n2 * ((n2 ! ) - 1)) / (n2 * 1) by A21, A25, XREAL_1:79;
then A40: n3 ! <= ((n2 ! ) - 1) / 1 by A21, A25, XCMPLX_1:92;
A41: [/c\] >= c by INT_1:def 5;
[/c\] + 1 > [/c\] + 0 by XREAL_1:10;
then [/c\] + 1 > c by A41, XXREAL_0:2;
then A42: n2 > c by A23, XXREAL_0:2;
A43: n3 ! > 0 by NEWTON:23;
2 * (n2 ! ) <= n2 * (n2 ! ) by A27, XREAL_1:66;
then 2 * (n2 ! ) < (n2 + 1) ! by A34, XXREAL_0:2;
then A44: 2 * n1 < (n2 + 1) ! by A37, XXREAL_0:2;
A45: f . (2 * n1) = Step1 (2 * n1) by A1
.= (n3 + 1) ! by A28, A44, A35, Def9
.= n2 * (n3 ! ) by NEWTON:21 ;
f . n1 = Step1 n1 by A1
.= n3 ! by A29, A36, A39, A40, Def9 ;
hence contradiction by A33, A32, A45, A42, A43, XREAL_1:70; :: thesis:

end;

take f ; :: thesis:

now

let n be Element of NAT ; :: thesis:
thus f . n <= (seq_n^ 1) . n :: thesis:

proof

per cases ;

suppose A46: n = 0 ; :: thesis:

f . 0 = Step1 0 by A1
.= 0 by Def9 ;
hence f . n <= (seq_n^ 1) . n by A46, Def3; :: thesis:

end;

suppose A47: n > 0 ; :: thesis:

then A48: (seq_n^ 1) . n = n to_power 1 by Def3
.= n by POWER:30 ;
ex n1 being Element of NAT st
( n1 ! <= n & n < (n1 + 1) ! & Step1 n = n1 ! ) by A47, Def9;
hence f . n <= (seq_n^ 1) . n by A1, A48; :: thesis:

end;

hence ( f = f & f is eventually-nondecreasing & ( for n being Element of NAT holds f . n <= (seq_n^ 1) . n ) & not f is smooth ) by A15, A17, ASYMPT_0:def 8; :: thesis: