Generalized Petersen graphs (#5005)

* Typos in comments for ~clnbgredg and ~clnbgrssedg

* Definition of generalized Petersen graphs and basic theorems

* ~fzo1lb added to main
* auxiliary theorems about module in AV's mathbox: ~difltmodne, ~zplusmodne, ~zp1modne , ~p1modne, ~addmodne
* definition of generalized Petersen graphs and basic theorems
* showing that `( N gPGr K )` are actually undirected simple graphs (~gpgusgra)

* Theorems about vertices and edges of generalized Petersen graphs

* ~ zltlem1d moved from MKU's mathbox to main set.mm
* ~ge2halflem1, ~elfzonn0elfzo, ~elfzo0subge1, ~elfzo0suble  added to main
* auxiliary theorems about module in AV's mathbox: ~submodlt,
* theorems about vertices and edges of generalized Petersen graphs

* The neighborhoods in a Petersen graph and a 5-prism are 3-stars

* ~ comraddi , ~mvrladdi  moved from DAW's mathbox to main set.mm
* ~prneimg2 , ~eluz4eluz3 , ~5eluz3 , ~muladdmod, ~addmulmodb, ~5ndvds3 , 5ndvds6  added to main
* auxiliary theorems about modulo in AV's mathbox: ~ceildivmod, ~ceil5half3, ~submodaddmod,  ~plusmod5ne, ~m1modne, ~minusmod5ne, ~submodneaddmod, ~m1modnep2mod, ~minusmodnep2tmod
* theorems about the ceiling of half of an integer:  +2ltceilhalf, ~ceilhalfelfzo1,  ~gpgedgvtx1lem
* Every generalized Petersen graph is a cubic_ graph: ~gpgcubic , ~gpgvtxdg3
* The closed neighborhoods in a generalized Petersen graph G(N,K) of order 10 (` N = 5 `) induce subgraphs which are isomorphic to 3-stars: ~gpg5nbgr3star

* proof of ~gpg3nbgrvtxlem shortened

* new theorem ~nn0le2x in main (generalization of ~nn0le2xi, proof of the latter shortened)
* new auxiliary theoem ~2tceilhalfelfzo1 in AV's mathbox
* proof of ~gpg3nbgrvtxlem shortened

* Rewrap

* discouraged

*  ~ax1ne0 replaced by ~ax-1n0 in proofs
* update discouraged file
* ~5rp moved from SN's mathbox to main

* review remarks by savask and GL

* icecream17's review remarks

* elfzonn0elfzo revised, renamed and moved
* elfzolem1 moved from GS's mathbox
* proofs of ~elfzo0subge1, ~elfzo0suble, ~elfzoext shortened
* typo gPetersonGr => gPetersenGr fixed

Author: avekens

changes-set.txt

@@ -92,10 +92,15 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+23-Sep-25 elfzolem1 [same]      moved from GS's mathbox to main set.mm
 11-Sep-25 cascl     [same]      revised - algSc may be non-injective
 10-Sep-25 soeq12d   [same]      Moved from SO's mathbox to main set.mm
 10-Sep-25 freq12d   [same]      Moved from SO's mathbox to main set.mm
 10-Sep-25 weeq12d   [same]      Moved from SO's mathbox to main set.mm
+ 9-Sep-25 5rp       [same]      moved from SN's mathbox to main set.mm
+ 8-Sep-25 mvrladdi  [same]      moved from DAW's mathbox to main set.mm
+ 8-Sep-25 comraddi  [same]      moved from DAW's mathbox to main set.mm
+ 8-Sep-25 zltlem1d  [same]      Moved from MKU's mathbox to main set.mm
  4-Sep-25 mhphf4    [same]      Removed unneeded hypotheses
  4-Sep-25 mhphf3    [same]      Removed unneeded hypotheses
  4-Sep-25 mhphf     [same]      Removed unneeded hypotheses

discouraged

@@ -16972,6 +16972,7 @@ New usage of "glbconxN" is discouraged (1 uses).
 New usage of "goeqi" is discouraged (0 uses).
 New usage of "golem1" is discouraged (1 uses).
 New usage of "golem2" is discouraged (1 uses).
+New usage of "gpg3nbgrvtx0ALT" is discouraged (0 uses).
 New usage of "grothac" is discouraged (1 uses).
 New usage of "grothomex" is discouraged (0 uses).
 New usage of "grothpw" is discouraged (0 uses).
@@ -21015,6 +21016,7 @@ Proof modification of "ggen31" is discouraged (22 steps).
 Proof modification of "ghomidOLD" is discouraged (178 steps).
 Proof modification of "ghomlinOLD" is discouraged (161 steps).
 Proof modification of "glbconNOLD" is discouraged (904 steps).
+Proof modification of "gpg3nbgrvtx0ALT" is discouraged (297 steps).
 Proof modification of "grpbaseOLD" is discouraged (11 steps).
 Proof modification of "grpinv11OLD" is discouraged (88 steps).
 Proof modification of "grpinvfvalALT" is discouraged (161 steps).