let k, n be Nat; :: thesis: (k * n) mod k = 0

per cases ( k = 0 or k <> 0 ) ;

suppose k = 0 ; :: thesis: (k * n) mod k = 0

hence (k * n) mod k = 0 by Def2; :: thesis: verum

end;

suppose k <> 0 ; :: thesis: (k * n) mod k = 0

then ( k * n = (k * n) + 0 & 0 < k ) ;
hence (k * n) mod k = 0 by Def2; :: thesis: verum

end;

end;