let n be non zero Nat; :: thesis:
let k, l be Nat; :: thesis:
assume A1: k mod n = l mod n ; :: thesis:

now :: thesis:

per cases by XXREAL_0:1;

suppose A2: k = l ; :: thesis:

set s = 0 ;
k = l + (0 * n) by A2;
hence ex s being Integer st k = l + (s * n) ; :: thesis:

end;

suppose A3: ( k > l or l > k ) ; :: thesis:

now :: thesis:

per cases by A3;

suppose k > l ; :: thesis:

hence ex s being Integer st k = l + (s * n) by A1, Lm1; :: thesis:

end;

suppose k < l ; :: thesis:

then consider t being Integer such that
A4: l = k + (t * n) by A1, Lm1;
k = l + ((- t) * n) by A4;
hence ex s being Integer st k = l + (s * n) ; :: thesis:

end;

end;

end;

hence ex s being Integer st k = l + (s * n) ; :: thesis:

end;

end;

end;

hence ex s being Integer st k = l + (s * n) ; :: thesis: