Intuitionize nndiv in iset.mm
Intuitionize nndiv in iset.mm

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

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