# Generated by tools/translator: qualified upstream name -> MoonBit name.
DEGREE_ZERO degree_zero
FINITE_LEMMA finite_lemma
HD_POLY_ADD hd_poly_add
HD_POLY_CMUL hd_poly_cmul
HD_POLY_EXP hd_poly_exp
HD_POLY_EXP_X_SUC hd_poly_exp_x_suc
HD_POLY_MUL hd_poly_mul
HD_POLY_MUL_X hd_poly_mul_x
ITERATE_RADD_POLYADD iterate_radd_polyadd
LENGTH_POLY_DIFF length_poly_diff
LENGTH_POLY_DIFF_AUX length_poly_diff_aux
MONOIDAL_POLY_ADD monoidal_poly_add
NOT_POLY_CMUL_NIL not_poly_cmul_nil
NOT_POLY_EXP_NIL not_poly_exp_nil
NOT_POLY_EXP_X_NIL not_poly_exp_x_nil
NOT_POLY_MUL_NIL not_poly_mul_nil
ORDER order_v1
ORDER_DECOMP order_decomp
ORDER_DIFF order_diff
ORDER_DIVIDES order_divides
ORDER_MUL order_mul
ORDER_POLY order_poly
ORDER_ROOT order_root
ORDER_THM order_thm
ORDER_UNIQUE order_unique
POLYDIFF_ADD polydiff_add
POLY_ADD poly_add_v1
POLY_ADD_ASSOC poly_add_assoc
POLY_ADD_CLAUSES poly_add_clauses
POLY_ADD_CONV poly_add_conv
POLY_ADD_IDENT poly_add_ident
POLY_ADD_LENGTH poly_add_length
POLY_ADD_NEUTRAL poly_add_neutral
POLY_ADD_RZERO poly_add_rzero
POLY_ADD_SYM poly_add_sym
POLY_CMUL poly_cmul_v1
POLY_CMUL_CLAUSES poly_cmul_clauses
POLY_CMUL_CONV poly_cmul_conv
POLY_CMUL_LENGTH poly_cmul_length
POLY_CMUL_LID poly_cmul_lid
POLY_CMUL_POLY_DIFF poly_cmul_poly_diff
POLY_CONST poly_const
POLY_CONT poly_cont
POLY_DIFF poly_diff_v1
POLY_DIFFERENTIABLE poly_differentiable
POLY_DIFF_ADD poly_diff_add
POLY_DIFF_AUX_ADD poly_diff_aux_add
POLY_DIFF_AUX_ADD_LEMMA poly_diff_aux_add_lemma
POLY_DIFF_AUX_CMUL poly_diff_aux_cmul
POLY_DIFF_AUX_ISZERO poly_diff_aux_iszero
POLY_DIFF_AUX_MUL_LEMMA poly_diff_aux_mul_lemma
POLY_DIFF_AUX_NEG poly_diff_aux_neg
POLY_DIFF_AUX_POLY_CMUL poly_diff_aux_poly_cmul
POLY_DIFF_CLAUSES poly_diff_clauses
POLY_DIFF_CMUL poly_diff_cmul
POLY_DIFF_CONV poly_diff_conv
POLY_DIFF_EXP poly_diff_exp
POLY_DIFF_EXP_PRIME poly_diff_exp_prime
POLY_DIFF_ISZERO poly_diff_iszero
POLY_DIFF_LEMMA poly_diff_lemma
POLY_DIFF_MUL poly_diff_mul
POLY_DIFF_MUL_LEMMA poly_diff_mul_lemma
POLY_DIFF_NEG poly_diff_neg
POLY_DIFF_WELLDEF poly_diff_welldef
POLY_DIFF_ZERO poly_diff_zero
POLY_DIVIDES_ADD poly_divides_add
POLY_DIVIDES_EXP poly_divides_exp
POLY_DIVIDES_REFL poly_divides_refl
POLY_DIVIDES_SUB poly_divides_sub
POLY_DIVIDES_SUB2 poly_divides_sub2
POLY_DIVIDES_TRANS poly_divides_trans
POLY_DIVIDES_ZERO poly_divides_zero
POLY_ENTIRE poly_entire
POLY_ENTIRE_LEMMA poly_entire_lemma
POLY_EXP poly_exp_v1
POLY_EXP_ADD poly_exp_add
POLY_EXP_DIVIDES poly_exp_divides
POLY_EXP_EQ_0 poly_exp_eq_0
POLY_EXP_PRIME_EQ_0 poly_exp_prime_eq_0
POLY_EXP_X_LENGTH poly_exp_x_length
POLY_EXP_X_REC poly_exp_x_rec
POLY_IVT_NEG poly_ivt_neg
POLY_IVT_POS poly_ivt_pos
POLY_LENGTH_MUL poly_length_mul
POLY_LINEAR_DIVIDES poly_linear_divides
POLY_LINEAR_REM poly_linear_rem
POLY_MONO poly_mono
POLY_MUL poly_mul_v1
POLY_MUL_ASSOC poly_mul_assoc
POLY_MUL_CLAUSES poly_mul_clauses
POLY_MUL_CONV poly_mul_conv
POLY_MUL_LCANCEL poly_mul_lcancel
POLY_MUL_LENGTH poly_mul_length
POLY_MUL_LENGTH2 poly_mul_length2
POLY_MUL_LID poly_mul_lid
POLY_MUL_RID poly_mul_rid
POLY_MVT poly_mvt
POLY_MVT_ADD poly_mvt_add
POLY_NEG poly_neg_v1
POLY_NEG_CLAUSES poly_neg_clauses
POLY_NORMALIZE poly_normalize
POLY_NORMALIZE_CONV poly_normalize_conv
POLY_ORDER poly_order
POLY_ORDER_EXISTS poly_order_exists
POLY_PRIMES poly_primes
POLY_PRIME_EQ_0 poly_prime_eq_0
POLY_ROOTS_FINITE poly_roots_finite
POLY_ROOTS_FINITE_LEMMA poly_roots_finite_lemma
POLY_ROOTS_FINITE_SET poly_roots_finite_set
POLY_ROOTS_INDEX_LEMMA poly_roots_index_lemma
POLY_ROOTS_INDEX_LENGTH poly_roots_index_length
POLY_SQUAREFREE_DECOMP poly_squarefree_decomp
POLY_SQUAREFREE_DECOMP_ORDER poly_squarefree_decomp_order
POLY_SUM_EQUIV poly_sum_equiv
POLY_X poly_x
POLY_ZERO poly_zero
POLY_ZERO_LEMMA poly_zero_lemma
RSQUAREFREE_DECOMP rsquarefree_decomp
RSQUAREFREE_ROOTS rsquarefree_roots
TL_POLY_CMUL tl_poly_cmul
TL_POLY_EXP_X_SUC tl_poly_exp_x_suc
TL_POLY_MUL_X tl_poly_mul_x
degree degree
divides divides
normalize normalize
order order
poly poly
poly_add poly_add
poly_cmul poly_cmul
poly_diff poly_diff
poly_diff_aux poly_diff_aux
poly_exp poly_exp
poly_mul poly_mul
poly_neg poly_neg
rsquarefree rsquarefree
