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