let k, n, t be Nat; :: thesis: ( 1 <= t & k <= n & 2 * t divides k implies ( n div t is even iff (n -' k) div t is even ) )
assume that
A1: 1 <= t and
A2: k <= n and
A3: 2 * t divides k ; :: thesis: ( n div t is even iff (n -' k) div t is even )
consider r being Nat such that
A4: k = (2 * t) * r by A3, NAT_D:def 3;
thus ( n div t is even implies (n -' k) div t is even ) :: thesis: ( (n -' k) div t is even implies n div t is even )

proof

assume n div t is even ; :: thesis: (n -' k) div t is even
then consider p being Nat such that
A5: n div t = 2 * p by ABIAN:def 2;
consider q being Nat such that
A6: n = (t * (2 * p)) + q and
A7: q < t by A1, A5, NAT_D:def 1;
1 * t < 2 * t by A1, XREAL_1:68;
then t + q < (2 * t) + t by A7, XREAL_1:8;
then q < 2 * t by XREAL_1:6;
then q / (2 * t) < 1 by XREAL_1:189;
then A8: p + (q / (2 * t)) < p + 1 by XREAL_1:6;
consider r being Nat such that
A9: k = (2 * t) * r by A3, NAT_D:def 3;
A10: 2 * t <> 0 by A1;
then (2 * t) * r <= ((2 * t) * p) + ((q / (2 * t)) * (2 * t)) by A2, A6, A9, XCMPLX_1:87;
then (2 * t) * r <= (2 * t) * (p + (q / (2 * t))) ;
then r <= p + (q / (2 * t)) by A10, XREAL_1:68;
then (p + (q / (2 * t))) + r < (p + 1) + (p + (q / (2 * t))) by A8, XREAL_1:8;
then r < p + 1 by XREAL_1:6;
then A11: r <= p by NAT_1:13;
n -' k = ((t * (2 * p)) + q) - ((2 * t) * r) by A2, A6, A9, XREAL_1:233
.= (t * (2 * (p - r))) + q
.= (t * (2 * (p -' r))) + q by A11, XREAL_1:233 ;
hence (n -' k) div t is even by A7, NAT_D:def 1; :: thesis: verum

end;

assume (n -' k) div t is even ; :: thesis: n div t is even
then consider p being Nat such that
A12: (n -' k) div t = 2 * p by ABIAN:def 2;
consider q being Nat such that
A13: n -' k = (t * (2 * p)) + q and
A14: q < t by A1, A12, NAT_D:def 1;
n - k = (t * (2 * p)) + q by A2, A13, XREAL_1:233;
then n = (t * (2 * (p + r))) + q by A4;
hence n div t is even by A14, NAT_D:def 1; :: thesis: verum