let n, k, l be Nat; :: thesis: ( n <> 0 & k mod n = 0 & l < n implies (k + l) mod n = l )
assume that
A1: n <> 0 and
A2: k mod n = 0 and
A3: l < n ; :: thesis: (k + l) mod n = l
ex t being Nat st
( k = (n * t) + 0 & 0 < n ) by A1, A2, Def2;
hence (k + l) mod n = l by A3, Def2; :: thesis: verum