let k, n be Nat; :: thesis: ( k < n implies k mod n = k )
assume A1: k < n ; :: thesis: k mod n = k
ex p being Nat st
( k = (n * p) + k & k < n )

proof

k = (n * 0 ) + k ;
hence ex p being Nat st
( k = (n * p) + k & k < n ) by A1; :: thesis: verum

end;

hence k mod n = k by Def2; :: thesis: verum