let a be Nat; :: thesis: a mod 1 = 0
a = (1 * a) + 0 ;
hence a mod 1 = 0 by NAT_D:def 2; :: thesis: verum