let n be non zero Nat; :: thesis: for k, l being Nat st k mod n = l mod n holds
ex s being Integer st k = l + (s * n)
let k, l be Nat; :: thesis: ( k mod n = l mod n implies ex s being Integer st k = l + (s * n) )
assume A1: k mod n = l mod n ; :: thesis: ex s being Integer st k = l + (s * n)

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

per cases ( k = l or k > l or l > k ) by XXREAL_0:1;

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

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

end;

suppose A3: ( k > l or l > k ) ; :: thesis: ex s being Integer st k = l + (s * n)

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

per cases ( k > l or k < l ) by A3;

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

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

end;

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

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: verum

end;

end;

end;

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

end;

end;

end;

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