theorem :: NAT_2:23

for k, n, t being Nat st 1 <= t & k <= n & 2 * t divides k holds
( n div t is even iff (n -' k) div t is even )