Generalize rexdif1en and dif1en (#4543)

* Revise dif1enlem

* Revise rexdif1en

* Use revised rexdif1en in findcard2

* Revise dif1en

* Prove dif1ennn

* Use dif1ennn instead of dif1enOLD

* Rename dif1enALT to dif1ennnALT

discouraged

@@ -5292,6 +5292,9 @@
 "dicdmN" is used by "dicvalrelN".
 "dicelvalN" is used by "dicelval2N".
 "dicfnN" is used by "dicdmN".
+"dif1enOLD" is used by "findcard2OLD".
+"dif1enlemOLD" is used by "dif1enOLD".
+"dif1enlemOLD" is used by "rexdif1enOLD".
 "dihglbcN" is used by "dihmeetcN".
 "dihglbcpreN" is used by "dihglbcN".
 "dihglblem2N" is used by "dihglblem3N".
@@ -16113,7 +16116,9 @@ New usage of "dicelval2N" is discouraged (0 uses).
 New usage of "dicelvalN" is discouraged (1 uses).
 New usage of "dicfnN" is discouraged (1 uses).
 New usage of "dicvalrelN" is discouraged (0 uses).
-New usage of "dif1enALT" is discouraged (0 uses).
+New usage of "dif1enOLD" is discouraged (1 uses).
+New usage of "dif1enlemOLD" is discouraged (2 uses).
+New usage of "dif1ennnALT" is discouraged (0 uses).
 New usage of "difidALT" is discouraged (0 uses).
 New usage of "difopabOLD" is discouraged (0 uses).
 New usage of "dih0bN" is discouraged (0 uses).
@@ -18824,6 +18829,7 @@ New usage of "rexbiOLD" is discouraged (0 uses).
 New usage of "rexbidvALT" is discouraged (0 uses).
 New usage of "rexbidvaALT" is discouraged (0 uses).
 New usage of "rexcomOLD" is discouraged (0 uses).
+New usage of "rexdif1enOLD" is discouraged (0 uses).
 New usage of "reximdvaiOLD" is discouraged (0 uses).
 New usage of "reximiaOLD" is discouraged (0 uses).
 New usage of "rexlimddvcbv" is discouraged (0 uses).
@@ -20188,7 +20194,9 @@ Proof modification of "dfvd3anir" is discouraged (19 steps).
 Proof modification of "dfvd3i" is discouraged (19 steps).
 Proof modification of "dfvd3ir" is discouraged (19 steps).
 Proof modification of "dfwrecsOLD" is discouraged (619 steps).
-Proof modification of "dif1enALT" is discouraged (335 steps).
+Proof modification of "dif1enOLD" is discouraged (313 steps).
+Proof modification of "dif1enlemOLD" is discouraged (285 steps).
+Proof modification of "dif1ennnALT" is discouraged (335 steps).
 Proof modification of "difidALT" is discouraged (14 steps).
 Proof modification of "difopabOLD" is discouraged (171 steps).
 Proof modification of "dih2dimbALTN" is discouraged (450 steps).
@@ -21194,6 +21202,7 @@ Proof modification of "rexbiOLD" is discouraged (65 steps).
 Proof modification of "rexbidvALT" is discouraged (10 steps).
 Proof modification of "rexbidvaALT" is discouraged (10 steps).
 Proof modification of "rexcomOLD" is discouraged (67 steps).
+Proof modification of "rexdif1enOLD" is discouraged (120 steps).
 Proof modification of "reximdvaiOLD" is discouraged (28 steps).
 Proof modification of "reximiaOLD" is discouraged (21 steps).
 Proof modification of "rexlimivOLD" is discouraged (23 steps).