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