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 A1: k <> 0 ; :: thesis: (k * n) mod k = 0

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

end;

end;