let n be Nat; :: thesis: n div 1 = n
n = (1 * n) + 0 ;
hence n div 1 = n by NAT_D:def 1; :: thesis: verum