Fermat pseudoprimes and weak pseudoprimes (#3237)

* Fermat pseudoprimes and weak psodoprimes

main set.mm:
* ~eqneltri moved from GS's mathbox
* auxiliary theorems: ~eluz4eluz2, ~eluz4nn, ~ge2nprmge4

AV's mathbox:
* auxiliary theorems: ~m2even, ~ gcd2odd1, ~nneven, ~nnennexALTV,  ~nnennex
* definition ~df-fppr of Fermat pseudoprimes `FPPr` and basic theorems
* Fermat pseudoprimes to the base 2 (Poulet number): ~fppr2odd, ~341fppr2, ~fpprel2
* additional examples for Fermat pseudoprimes: ~4fppr1, ~9fppr8
* weak pseudoprimes: ~dfwppr, ~fpprwppr, ~fpprwpprb
* Fermat's little theorem reversed is not generally true: ~nfermltl8rev, ~nfermltl2rev, ~nfermltlrev

* Update changes-set.txt

* Minor corrections

* 9 proofs shortened using ~eqneltri

identified by the minimize-script

Author: avekens

changes-set.txt

@@ -27,6 +27,7 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+ 8-Jun-23 eqneltri  [same]      moved from GS's mathbox to main set.mm
  6-Jun-23 2sqmo     [same]      moved from TA's mathbox to main set.mm
  6-Jun-23 2sqmod    [same]      moved from TA's mathbox to main set.mm
  6-Jun-23 2sqn0     [same]      moved from TA's mathbox to main set.mm