sbbiiev + save ax-11 in sbco4 + misc trig (#5000)

* add and use sbbiiev

* misc unit circle identities + utils
+ shorten nfa1w

in particular lttrii seems to replace most uses of lttri

* fixes, prove tanhalfpim

* move cbvabv sbco4 up, save ax-11 in sbco4, rewrap

Author: icecream17

discouraged

@@ -19226,11 +19226,14 @@ New usage of "sbco" is discouraged (2 uses).
 New usage of "sbco2" is discouraged (6 uses).
 New usage of "sbco2d" is discouraged (1 uses).
 New usage of "sbco3" is discouraged (1 uses).
+New usage of "sbco4OLD" is discouraged (0 uses).
 New usage of "sbco4lemOLD" is discouraged (0 uses).
+New usage of "sbco4lemOLDOLD" is discouraged (0 uses).
 New usage of "sbcom" is discouraged (0 uses).
 New usage of "sbcom3" is discouraged (3 uses).
 New usage of "sbcoreleleq" is discouraged (2 uses).
 New usage of "sbcoreleleqVD" is discouraged (0 uses).
+New usage of "sbcovOLD" is discouraged (0 uses).
 New usage of "sbcrexgOLD" is discouraged (2 uses).
 New usage of "sbcssgVD" is discouraged (0 uses).
 New usage of "sbel2x" is discouraged (0 uses).
@@ -19245,6 +19248,8 @@ New usage of "sbidm" is discouraged (0 uses).
 New usage of "sbie" is discouraged (20 uses).
 New usage of "sbied" is discouraged (3 uses).
 New usage of "sbiedv" is discouraged (1 uses).
+New usage of "sbievOLD" is discouraged (0 uses).
+New usage of "sbievwOLD" is discouraged (0 uses).
 New usage of "sbn1ALT" is discouraged (0 uses).
 New usage of "sbnfOLD" is discouraged (0 uses).
 New usage of "sbralieALT" is discouraged (0 uses).
@@ -19565,6 +19570,7 @@ New usage of "syl5imp" is discouraged (0 uses).
 New usage of "syl5impVD" is discouraged (0 uses).
 New usage of "symgsubmefmndALT" is discouraged (0 uses).
 New usage of "symgvalstructOLD" is discouraged (0 uses).
+New usage of "tan4thpiOLD" is discouraged (0 uses).
 New usage of "tarski-bernays-ax2" is discouraged (0 uses).
 New usage of "taylply2OLD" is discouraged (0 uses).
 New usage of "taylthlem2OLD" is discouraged (0 uses).
@@ -21606,12 +21612,17 @@ Proof modification of "sbcim1OLD" is discouraged (33 steps).
 Proof modification of "sbcim2g" is discouraged (83 steps).
 Proof modification of "sbcim2gVD" is discouraged (139 steps).
 Proof modification of "sbcimdvOLD" is discouraged (52 steps).
-Proof modification of "sbco4lemOLD" is discouraged (98 steps).
+Proof modification of "sbco4OLD" is discouraged (79 steps).
+Proof modification of "sbco4lemOLD" is discouraged (66 steps).
+Proof modification of "sbco4lemOLDOLD" is discouraged (98 steps).
 Proof modification of "sbcoreleleq" is discouraged (91 steps).
 Proof modification of "sbcoreleleqVD" is discouraged (176 steps).
+Proof modification of "sbcovOLD" is discouraged (32 steps).
 Proof modification of "sbcrexgOLD" is discouraged (77 steps).
 Proof modification of "sbcssgVD" is discouraged (229 steps).
 Proof modification of "sbhypfOLD" is discouraged (58 steps).
+Proof modification of "sbievOLD" is discouraged (24 steps).
+Proof modification of "sbievwOLD" is discouraged (23 steps).
 Proof modification of "sbn1ALT" is discouraged (41 steps).
 Proof modification of "sbnfOLD" is discouraged (82 steps).
 Proof modification of "sbralieALT" is discouraged (98 steps).
@@ -21706,6 +21717,7 @@ Proof modification of "syl5impVD" is discouraged (57 steps).
 Proof modification of "symgsubmefmndALT" is discouraged (129 steps).
 Proof modification of "symgvalstructOLD" is discouraged (651 steps).
 Proof modification of "symrefref3" is discouraged (75 steps).
+Proof modification of "tan4thpiOLD" is discouraged (135 steps).
 Proof modification of "tarski-bernays-ax2" is discouraged (557 steps).
 Proof modification of "taylply2OLD" is discouraged (657 steps).
 Proof modification of "taylthlem2OLD" is discouraged (2711 steps).