let m, n be Nat; :: thesis: ( 2 |^ m divides 2 |^ n implies m <= n )
( not m <= n implies not 2 |^ m divides 2 |^ n )

proof

assume A1: not m <= n ; :: thesis: not 2 |^ m divides 2 |^ n
not 2 |^ m divides 2 |^ n

proof

assume A2: 2 |^ m divides 2 |^ n ; :: thesis: contradiction
(2 |^ n) div (2 |^ m) = 0 by A1, Lm13, NAT_D:27;
then 2 |^ n > (2 |^ m) * ((2 |^ n) div (2 |^ m)) by PREPOWER:13;
hence contradiction by A2, NAT_D:3; :: thesis: verum

end;

hence not 2 |^ m divides 2 |^ n ; :: thesis: verum

end;

hence ( 2 |^ m divides 2 |^ n implies m <= n ) ; :: thesis: verum