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;