let n be Nat; :: thesis: ( n <> 0 implies n div n = 1 )
assume n <> 0 ; :: thesis: n div n = 1
then (n * 1) div n = 1 by NAT_D:18;
hence n div n = 1 ; :: thesis: verum