let a, b be Nat; :: thesis: a mod b <= a

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

suppose b = 0 ; :: thesis: a mod b <= a

hence a mod b <= a ; :: thesis: verum

end;

suppose b <> 0 ; :: thesis: a mod b <= a

then reconsider b = b as non zero Nat ;
((a div b) * b) + (a mod b) >= 0 + (a mod b) by XREAL_1:6;
hence a mod b <= a by NAT_D:2; :: thesis: verum

end;

end;