Intuitionize fzm1 in iset.mm
Intuitionize fzm1 in iset.mm

The set.mm proof relies on orrd. The new proof is pretty much
different; the most obvious thing the two proofs have in common
is using npcan to show ( ( N - 1 ) + 1 ) = N .

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