theory lemmas as well as additional properties of the SM2 elliptic
curve (to make this consistent with the files for the NIST curves):

        ETA_ONE
        FIELD_HOMOMORPHISM_DIV
        FIELD_HOMOMORPHISM_INV
        FINITE_MONOMIAL_VARS
        FINITE_MONOMIAL_VARS_1
        IMAGE_POLY_EVAL
        IMAGE_POLY_EXTEND_1
        IN_IDEAL_GENERATED_SELF
        IN_IDEAL_GENERATED_SING
        IN_IDEAL_GENERATED_SING_EQ
        ISOMORPHIC_TRANSPORT_OF_RING
        POLY_DEG_SUBRING_GENERATED
        POLY_EXTEND_FROM_SUBRING_GENERATED
        POLY_EXTEND_INTO_SUBRING_GENERATED
        POLY_SUBRING_GENERATED_1
        POLY_SUBRING_GENERATED_CLAUSES
        PRIME_POWER_EXISTS_ALT
        RING_0_IN_SUBRING_GENERATED
        RING_1_IN_SUBRING_GENERATED
        RING_ADD_IN_SUBRING_GENERATED
        RING_HOMOMORPHISM_INV
        RING_MONOMORPHISM_INTO_SUBRING
        RING_MUL_IN_SUBRING_GENERATED
        RING_NEG_IN_SUBRING_GENERATED
        RING_POW_IN_SUBRING_GENERATED
        RING_PRODUCT_SUBRING_GENERATED
        RING_PRODUCT_SUBRING_GENERATED_GEN
        RING_SUM_CASES
        SM2_GROUP_ELEMENT_ORDER
        SM2_GROUP_ORDER
        SUBRING_GENERATED_INC_GEN