let m, n be Nat; :: thesis: ( 1 <= m implies 1 <= m to_power n )

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: ( 1 <= m implies 1 <= m to_power n )

hence ( 1 <= m implies 1 <= m to_power n ) by POWER:24; :: thesis: verum

end;

suppose A1: n <> 0 ; :: thesis: ( 1 <= m implies 1 <= m to_power n )

assume 1 <= m ; :: thesis: 1 <= m to_power n
then ( 1 < m or 1 = m ) by XXREAL_0:1;
hence 1 <= m to_power n by A1, POWER:26, POWER:35; :: thesis: verum

end;

end;