Add lemmas, reduce axiom usage, shorten proofs

[GinoGiotto]

This PR contains the following changes:

• Add rspw -> use it in the proof of solin to avoid ax-12.

• Add vtocl3g -> use it in the proof of vtocl3ga to avoid ax-10 , ax-11 , ax-12

• Add ab0w -> use it in the proof of rabeq0w to shorten its proof and use it in the proofs of 0mpo0, fsetdmprc0 to avoid ax-10, ax-11, ax-12.

• Shorten proof of 0nelopab and avoid ax-10, ax-11, ax-12.

• Shorten proof of pocl and avoid ax-12 (ax-10 and ax-11 are automatically removed by editing vtocl3ga).

• Avoid ax-10, ax-11, ax-12 in dffr2, but add ax-8. All theorems using dffr2 depend on ax-8 anyway, so this does not affect them. The original proof of dffr2 is kept as dffr2ALT.

• Prove peano5 without ax-10, ax-12.

---

Results:
Drop ax-12 from 304 theorems.
Drop ax-11 from 135 theorems.
Drop ax-10 from 304 theorems.

Axiom usage here: d486acf