# Generated by tools/translator: qualified upstream name -> MoonBit name.
ABS_0 abs_0
ABS_1 abs_1
ABS_ABS abs_abs
ABS_BETWEEN abs_between
ABS_BETWEEN1 abs_between1
ABS_BETWEEN2 abs_between2
ABS_BOUND abs_bound
ABS_BOUNDS abs_bounds
ABS_CASES abs_cases
ABS_CIRCLE abs_circle
ABS_DIV abs_div
ABS_INV abs_inv
ABS_LE abs_le
ABS_LT_MUL2 abs_lt_mul2
ABS_MUL abs_mul
ABS_N abs_n
ABS_NEG abs_neg
ABS_NEG_LEMMA abs_neg_lemma
ABS_NZ abs_nz
ABS_POS abs_pos
ABS_POW2 abs_pow2
ABS_REFL abs_refl
ABS_SIGN abs_sign
ABS_SIGN2 abs_sign2
ABS_STILLNZ abs_stillnz
ABS_SUB abs_sub
ABS_SUB_ABS abs_sub_abs
ABS_SUM abs_sum
ABS_TRIANGLE abs_triangle
ABS_ZERO abs_zero
AND_FORALL_CONV and_forall_conv
BALL_NEIGH ball_neigh
BALL_OPEN ball_open
BOLZANO_LEMMA bolzano_lemma
BOLZANO_LEMMA_ALT bolzano_lemma_alt
CLOSED_LIMPT closed_limpt
COMPL_MEM compl_mem
CONTL contl_v1
CONTL_LIM contl_lim
CONTL_SEQ contl_seq
CONT_ABS cont_abs
CONT_ADD cont_add
CONT_ATTAINS cont_attains
CONT_ATTAINS2 cont_attains2
CONT_ATTAINS_ALL cont_attains_all
CONT_BOUNDED cont_bounded
CONT_BOUNDED_ABS cont_bounded_abs
CONT_COMPOSE cont_compose
CONT_CONST cont_const
CONT_DIV cont_div
CONT_HASSUP cont_hassup
CONT_INJ_LEMMA cont_inj_lemma
CONT_INJ_LEMMA2 cont_inj_lemma2
CONT_INJ_RANGE cont_inj_range
CONT_INV cont_inv
CONT_INVERSE cont_inverse
CONT_MUL cont_mul
CONT_NEG cont_neg
CONT_SUB cont_sub
CONT_UNIFORM cont_uniform
CONT_UNIFORM_STRONG cont_uniform_strong
CONT_X cont_x
CONV_OF_RCONV conv_of_rconv
CONV_OF_THM conv_of_thm
DIFF_ADD diff_add
DIFF_CARAT diff_carat
DIFF_CHAIN diff_chain
DIFF_CMUL diff_cmul
DIFF_CONST diff_const
DIFF_CONT diff_cont
DIFF_DIV diff_div
DIFF_INV diff_inv
DIFF_INVERSE diff_inverse
DIFF_INVERSE_LT diff_inverse_lt
DIFF_ISCONST diff_isconst
DIFF_ISCONST_ALL diff_isconst_all
DIFF_ISCONST_END diff_isconst_end
DIFF_ISCONST_END_SIMPLE diff_isconst_end_simple
DIFF_LCONST diff_lconst
DIFF_LDEC diff_ldec
DIFF_LINC diff_linc
DIFF_LMAX diff_lmax
DIFF_LMIN diff_lmin
DIFF_MUL diff_mul
DIFF_NEG diff_neg
DIFF_POW diff_pow
DIFF_SUB diff_sub
DIFF_SUM diff_sum
DIFF_UNIQ diff_uniq
DIFF_X diff_x
DIFF_XM1 diff_xm1
DORDER_LEMMA dorder_lemma
DORDER_NGE dorder_nge
DORDER_TENDSTO dorder_tendsto
DORDER_THEN dorder_then
EQUAL_TAC equal_tac
EXACT_CONV exact_conv
EXISTS_AND_CONV exists_and_conv
EXISTS_UNIQUE_CONV exists_unique_conv
EXPAND_TAC expand_tac
EXT_CONV ext_conv
FORALL_IMP_CONV forall_imp_conv
FUN_EQ_CONV fun_eq_conv
F_IMP f_imp
GP gp
GP_FINITE gp_finite
HABS_CONV habs_conv
HALF_MK_ABS half_mk_abs
IMP_SUBST_TAC imp_subst_tac
INST_TY_TERM inst_ty_term
INTERVAL_ABS interval_abs
INTERVAL_LEMMA interval_lemma
INTERVAL_LEMMA_LT interval_lemma_lt
ISMET_R1 ismet_r1
IVT ivt
IVT2 ivt2
IVT_DERIVATIVE_0 ivt_derivative_0
IVT_DERIVATIVE_NEG ivt_derivative_neg
IVT_DERIVATIVE_POS ivt_derivative_pos
LEFT_AND_EXISTS_CONV left_and_exists_conv
LEFT_AND_OVER_OR left_and_over_or
LEFT_IMP_EXISTS_CONV left_imp_exists_conv
LESS_0_CASES less_0_cases
LESS_ADD_1 less_add_1
LESS_ADD_SUC less_add_suc
LESS_CASES_IMP less_cases_imp
LESS_EQUAL_ADD less_equal_add
LESS_EQUAL_ANTISYM less_equal_antisym
LESS_EQ_IMP_LESS_SUC less_eq_imp_less_suc
LESS_EQ_SUC_REFL less_eq_suc_refl
LESS_LEMMA1 less_lemma1
LESS_LESS_CASES less_less_cases
LESS_MONO_ADD less_mono_add
LESS_OR less_or
LESS_SUC less_suc
LESS_SUC_REFL less_suc_refl
LIM lim_v1
LIM_ADD lim_add
LIM_CONST lim_const
LIM_DIV lim_div
LIM_EQUAL lim_equal
LIM_INV lim_inv
LIM_MUL lim_mul
LIM_NEG lim_neg
LIM_NULL lim_null
LIM_SUB lim_sub
LIM_SUM lim_sum
LIM_TENDS lim_tends
LIM_TENDS2 lim_tends2
LIM_TRANSFORM lim_transform
LIM_UNIQ lim_uniq
LIM_X lim_x
MAX_LEMMA max_lemma
METRIC_ISMET metric_ismet
METRIC_NZ metric_nz
METRIC_POS metric_pos
METRIC_SAME metric_same
METRIC_SYM metric_sym
METRIC_TRIANGLE metric_triangle
METRIC_ZERO metric_zero
MK_ABS mk_abs
MONO_SUC mono_suc
MR1_ADD mr1_add
MR1_ADD_LE mr1_add_le
MR1_ADD_LT mr1_add_lt
MR1_BETWEEN1 mr1_between1
MR1_BOUNDED mr1_bounded
MR1_DEF mr1_def
MR1_LIMPT mr1_limpt
MR1_SUB mr1_sub
MR1_SUB_LE mr1_sub_le
MR1_SUB_LT mr1_sub_lt
MTOP_LIMPT mtop_limpt
MTOP_OPEN mtop_open
MTOP_TENDS mtop_tends
MTOP_TENDS_UNIQ mtop_tends_uniq
MVT mvt
MVT_ALT mvt_alt
MVT_LEMMA mvt_lemma
NEST_LEMMA nest_lemma
NEST_LEMMA_UNIQ nest_lemma_uniq
NET_ABS net_abs
NET_ADD net_add
NET_CONV_BOUNDED net_conv_bounded
NET_CONV_IBOUNDED net_conv_ibounded
NET_CONV_NZ net_conv_nz
NET_DIV net_div
NET_INV net_inv
NET_LE net_le
NET_MUL net_mul
NET_NEG net_neg
NET_NULL net_null
NET_NULL_ADD net_null_add
NET_NULL_CMUL net_null_cmul
NET_NULL_MUL net_null_mul
NET_SUB net_sub
NET_SUM net_sum
NOT_EXISTS_CONV not_exists_conv
NOT_FORALL_CONV not_forall_conv
NOT_LESS_0 not_less_0
NOT_MP not_mp
NOT_SUC_LESS_EQ not_suc_less_eq
OLD_SKOLEM_CONV old_skolem_conv
OPEN_NEIGH open_neigh
OPEN_OWN_NEIGH open_own_neigh
OPEN_SUBOPEN open_subopen
OPEN_UNOPEN open_unopen
OR_LESS or_less
POW_0 pow_0
POW_1 pow_1
POW_2 pow_2
POW_2_LE1 pow_2_le1
POW_2_LT pow_2_lt
POW_ABS pow_abs
POW_ADD pow_add
POW_INV pow_inv
POW_LE pow_le
POW_M1 pow_m1
POW_MINUS1 pow_minus1
POW_MUL pow_mul
POW_NZ pow_nz
POW_PLUS1 pow_plus1
POW_POS pow_pos
POW_POS_LT pow_pos_lt
PSUM_SUM psum_sum
PSUM_SUM_NUMSEG psum_sum_numseg
REAL real
REAL_10 real_10
REAL_ADD real_add
REAL_ADD_LID_UNIQ real_add_lid_uniq
REAL_ADD_RID_UNIQ real_add_rid_uniq
REAL_ARCH real_arch
REAL_ARCH_LEAST real_arch_least
REAL_ARCH_POW real_arch_pow
REAL_ARCH_POW2 real_arch_pow2
REAL_ARCH_SIMPLE real_arch_simple
REAL_DIV_LZERO real_div_lzero
REAL_DIV_MUL2 real_div_mul2
REAL_DOUBLE real_double
REAL_EQ_LADD real_eq_ladd
REAL_EQ_LMUL real_eq_lmul
REAL_EQ_LMUL2 real_eq_lmul2
REAL_EQ_LMUL_IMP real_eq_lmul_imp
REAL_EQ_NEG real_eq_neg
REAL_EQ_RADD real_eq_radd
REAL_EQ_RMUL real_eq_rmul
REAL_EQ_RMUL_IMP real_eq_rmul_imp
REAL_FACT_NZ real_fact_nz
REAL_HALF_DOUBLE real_half_double
REAL_HORNER_SUM_CONV real_horner_sum_conv
REAL_INJ real_inj
REAL_INV1 real_inv1
REAL_INVINV real_invinv
REAL_INV_1OVER real_inv_1over
REAL_INV_LT1 real_inv_lt1
REAL_INV_MUL_WEAK real_inv_mul_weak
REAL_INV_NZ real_inv_nz
REAL_INV_POS real_inv_pos
REAL_LDISTRIB real_ldistrib
REAL_LE real_le_v1
REAL_LE1_POW2 real_le1_pow2
REAL_LE_DOUBLE real_le_double
REAL_LE_LADD real_le_ladd
REAL_LE_LDIV real_le_ldiv
REAL_LE_LMUL_IMP real_le_lmul_imp
REAL_LE_LMUL_LOCAL real_le_lmul_local
REAL_LE_LT real_le_lt
REAL_LE_MUL real_le_mul
REAL_LE_MUL2V real_le_mul2v
REAL_LE_NEG2 real_le_neg2
REAL_LE_NEGL real_le_negl
REAL_LE_NEGR real_le_negr
REAL_LE_NEGTOTAL real_le_negtotal
REAL_LE_RADD real_le_radd
REAL_LE_RDIV real_le_rdiv
REAL_LE_REFL real_le_refl
REAL_LE_RMUL_EQ real_le_rmul_eq
REAL_LE_RMUL_IMP real_le_rmul_imp
REAL_LE_SQUARE real_le_square
REAL_LE_SQUARE_POW real_le_square_pow
REAL_LE_SUB_LADD real_le_sub_ladd
REAL_LE_SUB_RADD real_le_sub_radd
REAL_LE_TOTAL real_le_total
REAL_LE_TRANS real_le_trans
REAL_LINV_UNIQ real_linv_uniq
REAL_LNEG_UNIQ real_lneg_uniq
REAL_LT real_lt
REAL_LT1_POW2 real_lt1_pow2
REAL_LTE_ADD real_lte_add
REAL_LTE_ADD2 real_lte_add2
REAL_LTE_TRANS real_lte_trans
REAL_LT_01 real_lt_01
REAL_LT_1 real_lt_1
REAL_LT_ADD real_lt_add
REAL_LT_ADD1 real_lt_add1
REAL_LT_ADD2 real_lt_add2
REAL_LT_ADDNEG real_lt_addneg
REAL_LT_ADDNEG2 real_lt_addneg2
REAL_LT_ADD_SUB real_lt_add_sub
REAL_LT_ANTISYM real_lt_antisym
REAL_LT_FRACTION real_lt_fraction
REAL_LT_FRACTION_0 real_lt_fraction_0
REAL_LT_GT real_lt_gt
REAL_LT_HALF1 real_lt_half1
REAL_LT_HALF2 real_lt_half2
REAL_LT_IADD real_lt_iadd
REAL_LT_IMP_LE real_lt_imp_le
REAL_LT_IMP_NE real_lt_imp_ne
REAL_LT_IMP_NZ real_lt_imp_nz
REAL_LT_LADD real_lt_ladd
REAL_LT_LE real_lt_le
REAL_LT_LMUL_0 real_lt_lmul_0
REAL_LT_LMUL_EQ real_lt_lmul_eq
REAL_LT_LMUL_IMP real_lt_lmul_imp
REAL_LT_MUL2_ALT real_lt_mul2_alt
REAL_LT_MULTIPLE real_lt_multiple
REAL_LT_NEG2 real_lt_neg2
REAL_LT_NEGTOTAL real_lt_negtotal
REAL_LT_NZ real_lt_nz
REAL_LT_RADD real_lt_radd
REAL_LT_RDIV real_lt_rdiv
REAL_LT_RDIV_0 real_lt_rdiv_0
REAL_LT_RMUL_0 real_lt_rmul_0
REAL_LT_RMUL_EQ real_lt_rmul_eq
REAL_LT_RMUL_IMP real_lt_rmul_imp
REAL_LT_SUB_LADD real_lt_sub_ladd
REAL_LT_SUB_RADD real_lt_sub_radd
REAL_MEAN real_mean
REAL_MIDDLE1 real_middle1
REAL_MIDDLE2 real_middle2
REAL_MUL real_mul
REAL_MUL_LZERO real_mul_lzero
REAL_MUL_RID real_mul_rid
REAL_MUL_RINV real_mul_rinv
REAL_MUL_RZERO real_mul_rzero
REAL_NEG_0 real_neg_0
REAL_NEG_ADD real_neg_add
REAL_NEG_EQ real_neg_eq
REAL_NEG_EQ0 real_neg_eq0
REAL_NEG_GE0 real_neg_ge0
REAL_NEG_GT0 real_neg_gt0
REAL_NEG_INV real_neg_inv
REAL_NEG_LE0 real_neg_le0
REAL_NEG_LMUL real_neg_lmul
REAL_NEG_LT0 real_neg_lt0
REAL_NEG_MINUS1 real_neg_minus1
REAL_NEG_MUL2 real_neg_mul2
REAL_NEG_NEG real_neg_neg
REAL_NEG_RMUL real_neg_rmul
REAL_NEG_SUB real_neg_sub
REAL_NOT_LE real_not_le
REAL_NOT_LT real_not_lt
REAL_NZ_IMP_LT real_nz_imp_lt
REAL_POS real_pos
REAL_POSSQ real_possq
REAL_POW_LBOUND real_pow_lbound
REAL_RDISTRIB real_rdistrib
REAL_RINV_UNIQ real_rinv_uniq
REAL_RNEG_UNIQ real_rneg_uniq
REAL_SUB_0 real_sub_0
REAL_SUB_ABS real_sub_abs
REAL_SUB_ADD real_sub_add
REAL_SUB_ADD2 real_sub_add2
REAL_SUB_INV2 real_sub_inv2
REAL_SUB_LDISTRIB real_sub_ldistrib
REAL_SUB_LE real_sub_le
REAL_SUB_LNEG real_sub_lneg
REAL_SUB_LT real_sub_lt
REAL_SUB_LZERO real_sub_lzero
REAL_SUB_NEG2 real_sub_neg2
REAL_SUB_RDISTRIB real_sub_rdistrib
REAL_SUB_REFL real_sub_refl
REAL_SUB_RNEG real_sub_rneg
REAL_SUB_RZERO real_sub_rzero
REAL_SUB_SUB real_sub_sub
REAL_SUB_SUB2 real_sub_sub2
REAL_SUB_TRIANGLE real_sub_triangle
REAL_SUMSQ real_sumsq
REAL_SUM_CONV real_sum_conv
REAL_SUP real_sup
REAL_SUP_EXISTS real_sup_exists
REAL_SUP_LE real_sup_le
REAL_SUP_UBOUND real_sup_ubound
REAL_SUP_UBOUND_LE real_sup_ubound_le
RIGHT_AND_EXISTS_CONV right_and_exists_conv
RIGHT_AND_OVER_OR right_and_over_or
RIGHT_IMP_EXISTS_CONV right_imp_exists_conv
ROLLE rolle
SEQ seq
SEQ_ABS seq_abs
SEQ_ABS_IMP seq_abs_imp
SEQ_ADD seq_add
SEQ_BCONV seq_bconv
SEQ_BOUNDED seq_bounded
SEQ_BOUNDED_2 seq_bounded_2
SEQ_CAUCHY seq_cauchy
SEQ_CBOUNDED seq_cbounded
SEQ_CONST seq_const
SEQ_CONT_UNIFORM seq_cont_uniform
SEQ_DIRECT seq_direct
SEQ_DIV seq_div
SEQ_HARMONIC seq_harmonic
SEQ_ICONV seq_iconv
SEQ_INV seq_inv
SEQ_INV0 seq_inv0
SEQ_LE seq_le
SEQ_LE_0 seq_le_0
SEQ_LIM seq_lim
SEQ_MONOSUB seq_monosub
SEQ_MUL seq_mul
SEQ_NEG seq_neg
SEQ_NEG_BOUNDED seq_neg_bounded
SEQ_NEG_CONV seq_neg_conv
SEQ_NULL seq_null
SEQ_POW seq_pow
SEQ_POWER seq_power
SEQ_POWER_ABS seq_power_abs
SEQ_SBOUNDED seq_sbounded
SEQ_SUB seq_sub
SEQ_SUBLE seq_suble
SEQ_SUBSEQ seq_subseq
SEQ_SUC seq_suc
SEQ_SUM seq_sum
SEQ_TENDS seq_tends
SEQ_TRANSFORM seq_transform
SEQ_TRUNCATION seq_truncation
SEQ_UNIQ seq_uniq
SER_0 ser_0
SER_ABS ser_abs
SER_ACONV ser_aconv
SER_ADD ser_add
SER_CAUCHY ser_cauchy
SER_CDIV ser_cdiv
SER_CMUL ser_cmul
SER_COMPAR ser_compar
SER_COMPARA ser_compara
SER_COMPARA_UNIFORM ser_compara_uniform
SER_COMPARA_UNIFORM_WEAK ser_compara_uniform_weak
SER_GROUP ser_group
SER_LE ser_le
SER_LE2 ser_le2
SER_NEG ser_neg
SER_OFFSET ser_offset
SER_OFFSET_REV ser_offset_rev
SER_PAIR ser_pair
SER_POS_LE ser_pos_le
SER_POS_LT ser_pos_lt
SER_POS_LT_PAIR ser_pos_lt_pair
SER_RATIO ser_ratio
SER_SUB ser_sub
SER_UNIQ ser_uniq
SER_ZERO ser_zero
SETOK_LE_LT setok_le_lt
SINGLE_DEPTH_CONV single_depth_conv
SUBSEQ_SUC subseq_suc
SUBSETA_ANTISYM subseta_antisym
SUBSETA_REFL subseta_refl
SUBSETA_TRANS subseta_trans
SUBST subst
SUB_EQ_EQ_0 sub_eq_eq_0
SUB_LEFT_GREATER_EQ sub_left_greater_eq
SUB_LEFT_LESS_EQ sub_left_less_eq
SUB_LESS_EQ sub_less_eq
SUB_OLD sub_old
SUB_SUB sub_sub
SUC_SUB1 suc_sub1
SUMMABLE_SUM summable_sum
SUM_0 sum_0
SUM_1 sum_1
SUM_2 sum_2
SUM_ABS sum_abs
SUM_ABS_LE sum_abs_le
SUM_ADD sum_add
SUM_BOUND sum_bound
SUM_CANCEL sum_cancel
SUM_CMUL sum_cmul
SUM_CONST sum_const
SUM_DIFF sum_diff
SUM_DIFFERENCES_EQ sum_differences_eq
SUM_EQ sum_eq
SUM_EQ_0 sum_eq_0
SUM_GROUP sum_group
SUM_HORNER sum_horner
SUM_LE sum_le
SUM_MORETERMS_EQ sum_moreterms_eq
SUM_NEG sum_neg
SUM_NSUB sum_nsub
SUM_OFFSET sum_offset
SUM_POS sum_pos
SUM_POS_GEN sum_pos_gen
SUM_REINDEX sum_reindex
SUM_SPLIT sum_split
SUM_SUB sum_sub
SUM_SUBST sum_subst
SUM_SUMMABLE sum_summable
SUM_SWAP sum_swap
SUM_TWO sum_two
SUM_UNIQ sum_uniq
SUM_ZERO sum_zero
SUP_INTERVAL sup_interval
SYM_CANON_CONV sym_canon_conv
TOPOLOGY topology
TOPOLOGY_UNION topology_union
X_BETA_CONV x_beta_conv
X_FUN_EQ_CONV x_fun_eq_conv
X_SKOLEM_CONV x_skolem_conv
ball ball
bounded bounded
cauchy cauchy
closed closed
contl contl
convergent convergent
dest_neg_imp dest_neg_imp
differentiable differentiable
diffl diffl
dorder dorder
ismet ismet
istopology istopology
lim lim
limpt limpt
metric_tybij metric_tybij
mono mono
mr1 mr1
mtop mtop
mtop_istopology mtop_istopology
neigh neigh
pow pow
re_Union re_union
re_compl re_compl
re_intersect re_intersect
re_null re_null
re_subset re_subset
re_union re_union_v1
re_universe re_universe
real_le real_le
subseq subseq
sum sum
sum_DEF sum_def
sum_EXISTS sum_exists
suminf suminf
summable summable
sums sums
sup sup
sup_def sup_def
tends tends
tends_num_real tends_num_real
tends_real_real tends_real_real
tendsto tendsto
topology_tybij topology_tybij
