Metamath Proof Explorer
Table of Contents - 16.5.3. Theorems according to Mertzios and Unger
- 2pthfrgrrn
- 2pthfrgrrn2
- 2pthfrgr
- 3cyclfrgrrn1
- 3cyclfrgrrn
- 3cyclfrgrrn2
- 3cyclfrgr
- 4cycl2v2nb
- 4cycl2vnunb
- n4cyclfrgr
- 4cyclusnfrgr
- frgrnbnb
- frgrconngr
- vdgn0frgrv2
- vdgn1frgrv2
- vdgn1frgrv3
- vdgfrgrgt2