for m, i, n being Nat st 1 <= i holds
[\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Element of NAT