let n, m be Nat; :: thesis: ( n is even & m is even & n >= m implies tau_bar to_power n <= tau_bar to_power m )
assume A1: ( n is even & m is even & n >= m ) ; :: thesis: tau_bar to_power n <= tau_bar to_power m
then A2: n + 1 > m + 0 by XREAL_1:8;

per cases ( n = m or n > m ) by A2, 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 A3: n > m ; :: thesis: tau_bar to_power n <= tau_bar to_power m

then reconsider t = n - m as Nat by NAT_1:21;
A4: (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 Th2
.= ((tau_bar to_power t) - 1) * (tau_bar to_power m) ;
A5: tau_bar to_power m > 0 by Th6, A1;
n - m > m - m by A3, XREAL_1:9;
then tau_bar to_power t < 1 by Th8, XXREAL_0:2;
then (tau_bar to_power t) - 1 < 1 - 1 by XREAL_1:9;
then ((tau_bar to_power n) - (tau_bar to_power m)) + (tau_bar to_power m) < 0 + (tau_bar to_power m) by A4, A5, XREAL_1:6;
hence tau_bar to_power n <= tau_bar to_power m ; :: thesis: verum

end;

end;