Intuitionize nndivtr in iset.mm
Intuitionize nndivtr in iset.mm

The statement of the theorem is as in set.mm. The proof is the
set.mm one with not equal changed to apart.

metamath/set.mm,metamath/set.mm,metamath/set.mm