let k, n be Nat; :: thesis: ( k < n implies k mod n = k )
assume A1: k < n ; :: thesis: k mod n = k
k = (n * 0) + k ;
hence k mod n = k by A1, Def2; :: thesis: verum