let n be non zero Nat; :: thesis: n div n = 1
(n * 1) div n = 1 by NAT_D:18;
hence n div n = 1 ; :: thesis: verum