let k, m be Nat; :: thesis: ( (2 * k) + 1 <= m implies 2 to_power k <= (2 to_power m) / m )
assume A1: (2 * k) + 1 <= m ; :: thesis: 2 to_power k <= (2 to_power m) / m
2 * k <= (2 * k) + 1 by NAT_1:11;
then k + k <= m by A1, XXREAL_0:2;
then X1: (k + k) - k <= m - k by XREAL_1:9;
then m - k in NAT by INT_1:3;
then reconsider n = m - k as Nat ;
A2: n + k <= 2 to_power n by LMC31E, X1;
(2 to_power (n + k)) / (2 to_power n) <= (2 to_power (n + k)) / (n + k) by A1, A2, XREAL_1:118;
then 2 to_power ((n + k) - n) <= (2 to_power (n + k)) / (n + k) by POWER:29;
hence 2 to_power k <= (2 to_power m) / m ; :: thesis: verum