theorem :: PEPIN:31

for m, n being Nat holds
( m <= n iff 2 |^ m divides 2 |^ n ) by Lm6, Lm10;