Reduce ax-mulf usage 4 (#4772)

* reduce ax-mulf usage

* add ax.txt

* axiom usage comparison

* remove ax.txt

Author: GinoGiotto

discouraged

@@ -15741,6 +15741,7 @@ New usage of "cmtcomlemN" is discouraged (1 uses).
 New usage of "cmtfvalN" is discouraged (1 uses).
 New usage of "cmtidN" is discouraged (1 uses).
 New usage of "cmtvalN" is discouraged (4 uses).
+New usage of "cmvthOLD" is discouraged (0 uses).
 New usage of "cnaddabl" is discouraged (2 uses).
 New usage of "cnaddabloOLD" is discouraged (5 uses).
 New usage of "cnaddablx" is discouraged (0 uses).
@@ -18728,6 +18729,7 @@ New usage of "prstcnidlem" is discouraged (2 uses).
 New usage of "prstcocvalOLD" is discouraged (0 uses).
 New usage of "prstcval" is discouraged (2 uses).
 New usage of "prub" is discouraged (6 uses).
+New usage of "psercn2OLD" is discouraged (0 uses).
 New usage of "psrass1lemOLD" is discouraged (0 uses).
 New usage of "psrbagaddclOLD" is discouraged (1 uses).
 New usage of "psrbagconOLD" is discouraged (3 uses).
@@ -20193,6 +20195,7 @@ Proof modification of "cleljustALT" is discouraged (25 steps).
 Proof modification of "cleljustALT2" is discouraged (25 steps).
 Proof modification of "clelsb2OLD" is discouraged (63 steps).
 Proof modification of "clmgmOLD" is discouraged (50 steps).
+Proof modification of "cmvthOLD" is discouraged (1136 steps).
 Proof modification of "cnaddabloOLD" is discouraged (65 steps).
 Proof modification of "cnaddcom" is discouraged (71 steps).
 Proof modification of "cncvcOLD" is discouraged (38 steps).
@@ -21221,6 +21224,7 @@ Proof modification of "problem5" is discouraged (133 steps).
 Proof modification of "prstchom2ALT" is discouraged (121 steps).
 Proof modification of "prstclevalOLD" is discouraged (86 steps).
 Proof modification of "prstcocvalOLD" is discouraged (88 steps).
+Proof modification of "psercn2OLD" is discouraged (372 steps).
 Proof modification of "psrass1lemOLD" is discouraged (1513 steps).
 Proof modification of "psrbagaddclOLD" is discouraged (392 steps).
 Proof modification of "psrbagconOLD" is discouraged (365 steps).