set g = seq_n^ 3;
set f = seq_n^ 2;

assume seq_n^ 2 in Big_Omega (seq_n^ 3) ; :: thesis:
then consider s being Element of Funcs (NAT,REAL) such that
A1: s = seq_n^ 2 and
A2: ex d being Real ex N being Element of NAT st
( d > 0 & ( for n being Element of NAT st n >= N holds
( d * ((seq_n^ 3) . n) <= s . n & s . n >= 0 ) ) ) ;
consider d being Real, N being Element of NAT such that
A3: d > 0 and
A4: for n being Element of NAT st n >= N holds
( d * ((seq_n^ 3) . n) <= s . n & s . n >= 0 ) by A2;
A5: N + 2 > 1 + 0 by XREAL_1:8;
ex n being Element of NAT st
( n >= N & d * ((seq_n^ 3) . n) > s . n )

take n = max (N,[/((N + 2) / d)\]); :: thesis:
A6: n >= N by XXREAL_0:25;
A7: n is Integer by XXREAL_0:16;
A8: [/((N + 2) / d)\] >= (N + 2) / d by INT_1:def 7;
(N + 2) * (d ") > 0 * (d ") by A3, XREAL_1:68;
then A9: n > 0 by A8, XXREAL_0:25;
reconsider n = n as Element of NAT by A6, A7, INT_1:3;
A10: ((seq_n^ 2) . n) * (n to_power (- 2)) = (n to_power 2) * (n to_power (- 2)) by A9, Def3
.= n to_power (2 + (- 2)) by A9, POWER:27
.= 1 by POWER:24 ;
A11: n to_power (- 2) > 0 by A9, POWER:34;
A12: d * n >= d * [/((N + 2) / d)\] by A3, XREAL_1:64, XXREAL_0:25;
d * [/((N + 2) / d)\] >= d * ((N + 2) / d) by A3, A8, XREAL_1:64;
then d * n >= ((N + 2) / d) * d by A12, XXREAL_0:2;
then A13: d * n >= N + 2 by A3, XCMPLX_1:87;
(d * ((seq_n^ 3) . n)) * (n to_power (- 2)) = (d * (n to_power 3)) * (n to_power (- 2)) by A9, Def3
.= d * ((n to_power 3) * (n to_power (- 2)))
.= d * (n to_power (3 + (- 2))) by A9, POWER:27
.= d * n by POWER:25 ;
then (d * ((seq_n^ 3) . n)) * (n to_power (- 2)) > ((seq_n^ 2) . n) * (n to_power (- 2)) by A5, A10, A13, XXREAL_0:2;
hence ( n is set & n is Element of NAT & n >= N & d * ((seq_n^ 3) . n) > s . n ) by A1, A11, XREAL_1:64, XXREAL_0:25; :: thesis:

end;

end;