revise df-lring in (i)set.mm (#4670)

* minimize + typo

* move df-nzr up

* revise df-lring in (i)set.mm

The revision in iset.mm means that df-nzr is added to iset.mm
(Several theorems use df-hash but 01eq0ring can be changed to not use it,
making it intuitionizable)
(The shortening of nzrring could apply elsewhere, but this is out of scope.
The new proof is only shorter because the old proof needed eqid a bunch)

lringnz is revised to have `.1.` and `.0.` variables, not sure whether this
makes sense in iset.mm (causes aprap change)

lringuplu is revised to have fewer hypotheses (causes aprcotr change)

* add htmldef for NzRing

* move remaining theorems up

discouraged

@@ -14237,6 +14237,7 @@
 "znbaslemOLD" is used by "znmulOLD".
 "zrdivrng" is used by "dvrunz".
 New usage of "00sr" is discouraged (4 uses).
+New usage of "01eq0ringOLD" is discouraged (0 uses).
 New usage of "0bdop" is discouraged (2 uses).
 New usage of "0blo" is discouraged (1 uses).
 New usage of "0cnALT" is discouraged (0 uses).
@@ -18278,6 +18279,7 @@ New usage of "nvvop" is discouraged (3 uses).
 New usage of "nvz" is discouraged (9 uses).
 New usage of "nvz0" is discouraged (8 uses).
 New usage of "nvzcl" is discouraged (21 uses).
+New usage of "nzrringOLD" is discouraged (0 uses).
 New usage of "o2p2e4OLD" is discouraged (0 uses).
 New usage of "oc0" is discouraged (2 uses).
 New usage of "occl" is discouraged (15 uses).
@@ -19639,6 +19641,7 @@ New usage of "znbas2OLD" is discouraged (0 uses).
 New usage of "znbaslemOLD" is discouraged (3 uses).
 New usage of "znmulOLD" is discouraged (0 uses).
 New usage of "zrdivrng" is discouraged (1 uses).
+Proof modification of "01eq0ringOLD" is discouraged (150 steps).
 Proof modification of "0cnALT" is discouraged (82 steps).
 Proof modification of "0cnALT2" is discouraged (49 steps).
 Proof modification of "0cnALT3" is discouraged (3 steps).
@@ -21051,6 +21054,7 @@ Proof modification of "notnotrALT2" is discouraged (2 steps).
 Proof modification of "notnotrALTVD" is discouraged (34 steps).
 Proof modification of "notnotriALT" is discouraged (7 steps).
 Proof modification of "nsnlpligALT" is discouraged (110 steps).
+Proof modification of "nzrringOLD" is discouraged (22 steps).
 Proof modification of "o2p2e4OLD" is discouraged (67 steps).
 Proof modification of "odfvalALT" is discouraged (181 steps).
 Proof modification of "odubasOLD" is discouraged (62 steps).