i < 2 to_power n by A1;
then (2 to_power n) - i > i - i by XREAL_1:9;
then (2 to_power n) - i is Element of NAT by INT_1:3;
hence (2 to_power n) - i is Nat ; :: thesis: verum