# Generated by tools/translator: qualified upstream name -> MoonBit name.
BOUNDS_DIVIDED bounds_divided
BOUNDS_IGNORE bounds_ignore
BOUNDS_LINEAR bounds_linear
BOUNDS_LINEAR_0 bounds_linear_0
BOUNDS_NOTZERO bounds_notzero
DIST_ADD2 dist_add2
DIST_ADD2_REV dist_add2_rev
DIST_ADDBOUND dist_addbound
DIST_ELIM_THM dist_elim_thm
DIST_EQ_0 dist_eq_0
DIST_LADD dist_ladd
DIST_LADD_0 dist_ladd_0
DIST_LE_CASES dist_le_cases
DIST_LMUL dist_lmul
DIST_LZERO dist_lzero
DIST_RADD dist_radd
DIST_RADD_0 dist_radd_0
DIST_REFL dist_refl
DIST_RMUL dist_rmul
DIST_RZERO dist_rzero
DIST_SYM dist_sym
DIST_TRIANGLE dist_triangle
DIST_TRIANGLES_LE dist_triangles_le
DIST_TRIANGLE_LE dist_triangle_le
HREAL_ADD_AC hreal_add_ac
HREAL_ADD_ASSOC hreal_add_assoc
HREAL_ADD_LCANCEL hreal_add_lcancel
HREAL_ADD_LDISTRIB hreal_add_ldistrib
HREAL_ADD_LID hreal_add_lid
HREAL_ADD_RDISTRIB hreal_add_rdistrib
HREAL_ADD_RID hreal_add_rid
HREAL_ADD_SYM hreal_add_sym
HREAL_ARCH hreal_arch
HREAL_COMPLETE hreal_complete
HREAL_EQ_ADD_LCANCEL hreal_eq_add_lcancel
HREAL_EQ_ADD_RCANCEL hreal_eq_add_rcancel
HREAL_INV_0 hreal_inv_0
HREAL_LE_ADD hreal_le_add
HREAL_LE_ADD2 hreal_le_add2
HREAL_LE_ADD_LCANCEL hreal_le_add_lcancel
HREAL_LE_ADD_RCANCEL hreal_le_add_rcancel
HREAL_LE_ANTISYM hreal_le_antisym
HREAL_LE_EXISTS hreal_le_exists
HREAL_LE_EXISTS_DEF hreal_le_exists_def
HREAL_LE_MUL_RCANCEL_IMP hreal_le_mul_rcancel_imp
HREAL_LE_REFL hreal_le_refl
HREAL_LE_TOTAL hreal_le_total
HREAL_LE_TRANS hreal_le_trans
HREAL_MUL_ASSOC hreal_mul_assoc
HREAL_MUL_LID hreal_mul_lid
HREAL_MUL_LINV hreal_mul_linv
HREAL_MUL_LZERO hreal_mul_lzero
HREAL_MUL_RZERO hreal_mul_rzero
HREAL_MUL_SYM hreal_mul_sym
HREAL_OF_NUM_ADD hreal_of_num_add
HREAL_OF_NUM_EQ hreal_of_num_eq
HREAL_OF_NUM_LE hreal_of_num_le
HREAL_OF_NUM_MUL hreal_of_num_mul
NADD_ADD nadd_add_v1
NADD_ADDITIVE nadd_additive
NADD_ADD_ASSOC nadd_add_assoc
NADD_ADD_LCANCEL nadd_add_lcancel
NADD_ADD_LID nadd_add_lid
NADD_ADD_SYM nadd_add_sym
NADD_ADD_WELLDEF nadd_add_welldef
NADD_ALTMUL nadd_altmul
NADD_ARCH nadd_arch
NADD_ARCH_LEMMA nadd_arch_lemma
NADD_ARCH_MULT nadd_arch_mult
NADD_ARCH_ZERO nadd_arch_zero
NADD_BOUND nadd_bound
NADD_CAUCHY nadd_cauchy
NADD_COMPLETE nadd_complete
NADD_DIST nadd_dist
NADD_DIST_LEMMA nadd_dist_lemma
NADD_EQ_IMP_LE nadd_eq_imp_le
NADD_EQ_REFL nadd_eq_refl
NADD_EQ_SYM nadd_eq_sym
NADD_EQ_TRANS nadd_eq_trans
NADD_INV nadd_inv_v1
NADD_INV_0 nadd_inv_0
NADD_INV_WELLDEF nadd_inv_welldef
NADD_LBOUND nadd_lbound
NADD_LDISTRIB nadd_ldistrib
NADD_LE_0 nadd_le_0
NADD_LE_ADD nadd_le_add
NADD_LE_ANTISYM nadd_le_antisym
NADD_LE_EXISTS nadd_le_exists
NADD_LE_LADD nadd_le_ladd
NADD_LE_LMUL nadd_le_lmul
NADD_LE_RADD nadd_le_radd
NADD_LE_REFL nadd_le_refl
NADD_LE_RMUL nadd_le_rmul
NADD_LE_TOTAL nadd_le_total
NADD_LE_TOTAL_LEMMA nadd_le_total_lemma
NADD_LE_TRANS nadd_le_trans
NADD_LE_WELLDEF nadd_le_welldef
NADD_LE_WELLDEF_LEMMA nadd_le_welldef_lemma
NADD_MUL nadd_mul_v1
NADD_MULTIPLICATIVE nadd_multiplicative
NADD_MUL_ASSOC nadd_mul_assoc
NADD_MUL_LID nadd_mul_lid
NADD_MUL_LINV nadd_mul_linv
NADD_MUL_LINV_LEMMA0 nadd_mul_linv_lemma0
NADD_MUL_LINV_LEMMA1 nadd_mul_linv_lemma1
NADD_MUL_LINV_LEMMA2 nadd_mul_linv_lemma2
NADD_MUL_LINV_LEMMA3 nadd_mul_linv_lemma3
NADD_MUL_LINV_LEMMA4 nadd_mul_linv_lemma4
NADD_MUL_LINV_LEMMA5 nadd_mul_linv_lemma5
NADD_MUL_LINV_LEMMA6 nadd_mul_linv_lemma6
NADD_MUL_LINV_LEMMA7 nadd_mul_linv_lemma7
NADD_MUL_LINV_LEMMA7a nadd_mul_linv_lemma7a
NADD_MUL_LINV_LEMMA8 nadd_mul_linv_lemma8
NADD_MUL_SYM nadd_mul_sym
NADD_MUL_WELLDEF nadd_mul_welldef
NADD_MUL_WELLDEF_LEMMA nadd_mul_welldef_lemma
NADD_NONZERO nadd_nonzero
NADD_OF_NUM nadd_of_num_v1
NADD_OF_NUM_ADD nadd_of_num_add
NADD_OF_NUM_EQ nadd_of_num_eq
NADD_OF_NUM_LE nadd_of_num_le
NADD_OF_NUM_MUL nadd_of_num_mul
NADD_OF_NUM_WELLDEF nadd_of_num_welldef
NADD_RDISTRIB nadd_rdistrib
NADD_SUC nadd_suc
NADD_UBOUND nadd_ubound
REAL_ADD_ASSOC real_add_assoc
REAL_ADD_LDISTRIB real_add_ldistrib
REAL_ADD_LID real_add_lid
REAL_ADD_LINV real_add_linv
REAL_ADD_SYM real_add_sym
REAL_COMPLETE real_complete
REAL_COMPLETE_SOMEPOS real_complete_somepos
REAL_HREAL_LEMMA1 real_hreal_lemma1
REAL_HREAL_LEMMA2 real_hreal_lemma2
REAL_INV_0 real_inv_0
REAL_LE_ANTISYM real_le_antisym
REAL_LE_LADD_IMP real_le_ladd_imp
REAL_LE_MUL real_le_mul
REAL_LE_REFL real_le_refl
REAL_LE_TOTAL real_le_total
REAL_LE_TRANS real_le_trans
REAL_MUL_ASSOC real_mul_assoc
REAL_MUL_LID real_mul_lid
REAL_MUL_LINV real_mul_linv
REAL_MUL_SYM real_mul_sym
REAL_OF_NUM_ADD real_of_num_add
REAL_OF_NUM_EQ real_of_num_eq
REAL_OF_NUM_LE real_of_num_le
REAL_OF_NUM_MUL real_of_num_mul
TREAL_ADD_ASSOC treal_add_assoc
TREAL_ADD_LDISTRIB treal_add_ldistrib
TREAL_ADD_LID treal_add_lid
TREAL_ADD_LINV treal_add_linv
TREAL_ADD_SYM treal_add_sym
TREAL_ADD_SYM_EQ treal_add_sym_eq
TREAL_ADD_WELLDEF treal_add_welldef
TREAL_ADD_WELLDEFR treal_add_welldefr
TREAL_EQ_AP treal_eq_ap
TREAL_EQ_IMP_LE treal_eq_imp_le
TREAL_EQ_REFL treal_eq_refl
TREAL_EQ_SYM treal_eq_sym
TREAL_EQ_TRANS treal_eq_trans
TREAL_INV_0 treal_inv_0
TREAL_INV_WELLDEF treal_inv_welldef
TREAL_LE_ANTISYM treal_le_antisym
TREAL_LE_LADD_IMP treal_le_ladd_imp
TREAL_LE_MUL treal_le_mul
TREAL_LE_REFL treal_le_refl
TREAL_LE_TOTAL treal_le_total
TREAL_LE_TRANS treal_le_trans
TREAL_LE_WELLDEF treal_le_welldef
TREAL_MUL_ASSOC treal_mul_assoc
TREAL_MUL_LID treal_mul_lid
TREAL_MUL_LINV treal_mul_linv
TREAL_MUL_SYM treal_mul_sym
TREAL_MUL_SYM_EQ treal_mul_sym_eq
TREAL_MUL_WELLDEF treal_mul_welldef
TREAL_MUL_WELLDEFR treal_mul_welldefr
TREAL_NEG_WELLDEF treal_neg_welldef
TREAL_OF_NUM_ADD treal_of_num_add
TREAL_OF_NUM_EQ treal_of_num_eq
TREAL_OF_NUM_LE treal_of_num_le
TREAL_OF_NUM_MUL treal_of_num_mul
TREAL_OF_NUM_WELLDEF treal_of_num_welldef
dist dist
hreal_add hreal_add
hreal_add_th hreal_add_th
hreal_inv hreal_inv
hreal_inv_th hreal_inv_th
hreal_le hreal_le
hreal_le_th hreal_le_th
hreal_mul hreal_mul
hreal_mul_th hreal_mul_th
hreal_of_num hreal_of_num
hreal_of_num_th hreal_of_num_th
hreal_tybij hreal_tybij
is_nadd is_nadd
is_nadd_0 is_nadd_0
nadd_abs nadd_abs
nadd_add nadd_add
nadd_eq nadd_eq
nadd_inv nadd_inv
nadd_le nadd_le
nadd_mul nadd_mul
nadd_of_num nadd_of_num
nadd_rep nadd_rep
nadd_rinv nadd_rinv
prioritize_num prioritize_num
prioritize_real prioritize_real
real_abs real_abs
real_add real_add
real_add_th real_add_th
real_div real_div
real_ge real_ge
real_gt real_gt
real_inv real_inv
real_inv_th real_inv_th
real_le real_le
real_le_th real_le_th
real_lt real_lt
real_max real_max
real_min real_min
real_mul real_mul
real_mul_th real_mul_th
real_neg real_neg
real_neg_th real_neg_th
real_of_num real_of_num
real_of_num_th real_of_num_th
real_pow real_pow
real_sub real_sub
real_tybij real_tybij
treal_add treal_add
treal_eq treal_eq
treal_inv treal_inv
treal_le treal_le
treal_mul treal_mul
treal_neg treal_neg
treal_of_num treal_of_num
