let n, m be natural number ; :: thesis: ( not m is even & n >= m implies tau_bar to_power n >= tau_bar to_power m )
assume A1: not m is even ; :: thesis: ( not n >= m or tau_bar to_power n >= tau_bar to_power m )
assume n >= m ; :: thesis: tau_bar to_power n >= tau_bar to_power m
then zz: n + 1 > m + 0 by XREAL_1:10;

per cases ( n = m or n > m ) by zz, NAT_1:22;

suppose n = m ; :: thesis: tau_bar to_power n >= tau_bar to_power m

hence tau_bar to_power n >= tau_bar to_power m ; :: thesis: verum

end;

suppose A2: n > m ; :: thesis: tau_bar to_power n >= tau_bar to_power m

then reconsider t = n - m as natural number by NAT_1:21;
C2: (tau_bar to_power n) - (tau_bar to_power m) = (tau_bar to_power (t + m)) - (tau_bar to_power m)
.= ((tau_bar to_power t) * (tau_bar to_power m)) - (1 * (tau_bar to_power m)) by JakPower32
.= ((tau_bar to_power t) - 1) * (tau_bar to_power m) ;
C3: tau_bar to_power m <= 0 by pom2, A1;
t <> 0 by A2;
then ( abs tau_bar > 0 & t > 0 ) ;
then (abs tau_bar) to_power t < 1 to_power t by hop3, POWER:42;
then (abs tau_bar) to_power t < 1 by POWER:31;
then ( abs (tau_bar to_power t) < 1 & tau_bar to_power t <= abs (tau_bar to_power t) ) by ABSVALUE:11, SERIES_1:2;
then tau_bar to_power t < 1 by XXREAL_0:2;
then (tau_bar to_power t) - 1 <= 1 - 1 by XREAL_1:11;
then ((tau_bar to_power n) - (tau_bar to_power m)) + (tau_bar to_power m) >= 0 + (tau_bar to_power m) by C2, C3, XREAL_1:8;
hence tau_bar to_power n >= tau_bar to_power m ; :: thesis: verum

end;

end;