# Generated by tools/translator: qualified upstream name -> MoonBit name.
BEZOUT bezout
BEZOUT_ADD bezout_add
BEZOUT_ADD_STRONG bezout_add_strong
BEZOUT_GCD bezout_gcd
BEZOUT_GCD_STRONG bezout_gcd_strong
BEZOUT_PRIME bezout_prime
CHINESE_REMAINDER chinese_remainder
COMPLETE_FACTOR_INDUCT complete_factor_induct
CONG_MULT_LCANCEL_IFF cong_mult_lcancel_iff
CONG_MULT_RCANCEL_IFF cong_mult_rcancel_iff
COPRIME coprime
COPRIME_0 coprime_0
COPRIME_1 coprime_1
COPRIME_2 coprime_2
COPRIME_BEZOUT coprime_bezout
COPRIME_BEZOUT_ALT coprime_bezout_alt
COPRIME_BEZOUT_STRONG coprime_bezout_strong
COPRIME_CONV coprime_conv
COPRIME_DIVISORS coprime_divisors
COPRIME_DIVPROD coprime_divprod
COPRIME_DIVPROD_IFF coprime_divprod_iff
COPRIME_EXP coprime_exp
COPRIME_EXP2 coprime_exp2
COPRIME_EXP2_SUC coprime_exp2_suc
COPRIME_EXP_DIVPROD coprime_exp_divprod
COPRIME_EXP_IMP coprime_exp_imp
COPRIME_GCD coprime_gcd
COPRIME_INDEX coprime_index
COPRIME_LEXP coprime_lexp
COPRIME_LMUL coprime_lmul
COPRIME_LMUL2 coprime_lmul2
COPRIME_MINUS1 coprime_minus1
COPRIME_MUL coprime_mul
COPRIME_NPRODUCT coprime_nproduct
COPRIME_NPRODUCT_EQ coprime_nproduct_eq
COPRIME_PAIR_DECOMP coprime_pair_decomp
COPRIME_PLUS1 coprime_plus1
COPRIME_POW coprime_pow
COPRIME_PRIME coprime_prime
COPRIME_PRIMEPOW coprime_primepow
COPRIME_PRIME_EQ coprime_prime_eq
COPRIME_PRIME_PRIME coprime_prime_prime
COPRIME_REFL coprime_refl
COPRIME_REXP coprime_rexp
COPRIME_RMUL coprime_rmul
COPRIME_RMUL2 coprime_rmul2
COPRIME_SOS coprime_sos
COPRIME_SYM coprime_sym
DISTINCT_PRIME_COPRIME distinct_prime_coprime
DIVIDES_0 divides_0
DIVIDES_1 divides_1
DIVIDES_2 divides_2
DIVIDES_ADD divides_add
DIVIDES_ADD_REVL divides_add_revl
DIVIDES_ADD_REVR divides_add_revr
DIVIDES_CASES divides_cases
DIVIDES_CMUL2 divides_cmul2
DIVIDES_CONV divides_conv
DIVIDES_DIV_NOT divides_div_not
DIVIDES_EQ_ZERO divides_eq_zero
DIVIDES_EXP divides_exp
DIVIDES_EXP2 divides_exp2
DIVIDES_EXP2_EQ divides_exp2_eq
DIVIDES_EXP2_REV divides_exp2_rev
DIVIDES_EXP_LE divides_exp_le
DIVIDES_EXP_LE_IMP divides_exp_le_imp
DIVIDES_EXP_MINUS1 divides_exp_minus1
DIVIDES_EXP_PLUS1 divides_exp_plus1
DIVIDES_FACT divides_fact
DIVIDES_FACT_PRIME divides_fact_prime
DIVIDES_GCD divides_gcd
DIVIDES_GCD_LEFT divides_gcd_left
DIVIDES_GCD_RIGHT divides_gcd_right
DIVIDES_INDEX divides_index
DIVIDES_ITERATE_GCD divides_iterate_gcd
DIVIDES_ITERATE_GCD_GEN divides_iterate_gcd_gen
DIVIDES_ITERATE_LCM divides_iterate_lcm
DIVIDES_ITERATE_LCM_GEN divides_iterate_lcm_gen
DIVIDES_LCM divides_lcm
DIVIDES_LCM_GCD divides_lcm_gcd
DIVIDES_LCM_LEFT divides_lcm_left
DIVIDES_LCM_RIGHT divides_lcm_right
DIVIDES_LMUL divides_lmul
DIVIDES_LMUL2 divides_lmul2
DIVIDES_LMUL2_EQ divides_lmul2_eq
DIVIDES_LMUL_GCD divides_lmul_gcd
DIVIDES_MUL divides_mul
DIVIDES_MUL2 divides_mul2
DIVIDES_MUL_L divides_mul_l
DIVIDES_MUL_R divides_mul_r
DIVIDES_NSUM divides_nsum
DIVIDES_PRIMEPOW divides_primepow
DIVIDES_PRIME_EXP_LE divides_prime_exp_le
DIVIDES_PRIME_PRIME divides_prime_prime
DIVIDES_REFL divides_refl
DIVIDES_REXP divides_rexp
DIVIDES_REXP_SUC divides_rexp_suc
DIVIDES_RMUL divides_rmul
DIVIDES_RMUL2 divides_rmul2
DIVIDES_RMUL2_EQ divides_rmul2_eq
DIVIDES_RMUL_GCD divides_rmul_gcd
DIVIDES_SUB divides_sub
DIVIDES_SUB_1 divides_sub_1
DIVIDES_SUB_EQ divides_sub_eq
DIVIDES_TRANS divides_trans
DIVIDES_TRIVIAL_UPPERBOUND divides_trivial_upperbound
DIVIDES_ZERO divides_zero
DIVISION_DECOMP division_decomp
DIVISORS_EQ divisors_eq
EQ_INDEX eq_index
EQ_PRIMEPOW eq_primepow
EQ_PRIME_EXP eq_prime_exp
EUCLID euclid
EUCLID_BOUND euclid_bound
EXP_INDEX_DIVIDES exp_index_divides
EXP_MULT_EXISTS exp_mult_exists
FACTORIZATION_INDEX factorization_index
FINITE_DIVISORS finite_divisors
FINITE_EXP_LE finite_exp_le
FINITE_INDICES finite_indices
FINITE_SPECIAL_DIVISORS finite_special_divisors
FORALL_PRIME_INDEX forall_prime_index
GCD_0 gcd_0
GCD_1 gcd_1
GCD_2_CASES gcd_2_cases
GCD_ADD gcd_add
GCD_ASSOC gcd_assoc
GCD_BEZOUT gcd_bezout
GCD_BEZOUT_SUM gcd_bezout_sum
GCD_CONV gcd_conv
GCD_COPRIME gcd_coprime
GCD_COPRIME_DIVIDES_LMUL gcd_coprime_divides_lmul
GCD_COPRIME_DIVIDES_RMUL gcd_coprime_divides_rmul
GCD_COPRIME_EXISTS gcd_coprime_exists
GCD_COPRIME_LMUL gcd_coprime_lmul
GCD_COPRIME_RMUL gcd_coprime_rmul
GCD_EQ gcd_eq
GCD_EXP gcd_exp
GCD_LCM_DISTRIB gcd_lcm_distrib
GCD_LE gcd_le
GCD_LE_MAX gcd_le_max
GCD_LE_MIN gcd_le_min
GCD_LE_MIN_EQ gcd_le_min_eq
GCD_LMUL gcd_lmul
GCD_MULTIPLE gcd_multiple
GCD_MUL_COPRIME gcd_mul_coprime
GCD_ONE gcd_one
GCD_PRIME_CASES gcd_prime_cases
GCD_REFL gcd_refl
GCD_RMUL gcd_rmul
GCD_SUB gcd_sub
GCD_SYM gcd_sym
GCD_UNIQUE gcd_unique
GCD_ZERO gcd_zero
INDEX_0 index_0
INDEX_1 index_1
INDEX_ADD index_add
INDEX_ADD_MIN index_add_min
INDEX_DECOMPOSITION index_decomposition
INDEX_DECOMPOSITION_LE index_decomposition_le
INDEX_DECOMPOSITION_PRIME index_decomposition_prime
INDEX_DECOMPOSITION_UNIQUE index_decomposition_unique
INDEX_EQ_0 index_eq_0
INDEX_EXP index_exp
INDEX_FACT index_fact
INDEX_FACT_ALT index_fact_alt
INDEX_FACT_PRIME_MULT index_fact_prime_mult
INDEX_FACT_UNBOUNDED index_fact_unbounded
INDEX_GCD index_gcd
INDEX_LCM index_lcm
INDEX_LT index_lt
INDEX_MUL index_mul
INDEX_MULT_ADD index_mult_add
INDEX_MULT_BASE index_mult_base
INDEX_MULT_EXP index_mult_exp
INDEX_NSUM_LE index_nsum_le
INDEX_POW index_pow
INDEX_PRIME index_prime
INDEX_REFL index_refl
INDEX_SUB_MIN index_sub_min
INDEX_TRIVIAL_BOUND index_trivial_bound
INDEX_UNIQUE index_unique
INDEX_UNIQUE_ALT index_unique_alt
INDEX_UNIQUE_EQ index_unique_eq
INDEX_ZERO index_zero
INDUCT_COPRIME induct_coprime
INDUCT_COPRIME_ALT induct_coprime_alt
INDUCT_COPRIME_STRONG induct_coprime_strong
ITERATE_GCD_DIVIDES iterate_gcd_divides
ITERATE_GCD_DIVIDES_EQ iterate_gcd_divides_eq
ITERATE_GCD_EQ_0 iterate_gcd_eq_0
ITERATE_GCD_EQ_0_GEN iterate_gcd_eq_0_gen
ITERATE_LCM_DIVIDES iterate_lcm_divides
ITERATE_LCM_DIVIDES_GEN iterate_lcm_divides_gen
ITERATE_LCM_EQ_0 iterate_lcm_eq_0
ITERATE_LCM_EQ_0_GEN iterate_lcm_eq_0_gen
ITERATE_LCM_EQ_1 iterate_lcm_eq_1
ITERATE_LCM_EQ_1_GEN iterate_lcm_eq_1_gen
LCM lcm_v1
LCM_0 lcm_0
LCM_1 lcm_1
LCM_ASSOC lcm_assoc
LCM_CONV lcm_conv
LCM_COPRIME_DECOMP lcm_coprime_decomp
LCM_DIVIDES lcm_divides
LCM_DIVIDES_MUL lcm_divides_mul
LCM_EQ lcm_eq
LCM_EQ_1 lcm_eq_1
LCM_EQ_MULT lcm_eq_mult
LCM_EXP lcm_exp
LCM_GCD_DISTRIB lcm_gcd_distrib
LCM_LE_MULT lcm_le_mult
LCM_LMUL lcm_lmul
LCM_MULTIPLE lcm_multiple
LCM_REFL lcm_refl
LCM_RMUL lcm_rmul
LCM_SYM lcm_sym
LCM_UNIQUE lcm_unique
LCM_ZERO lcm_zero
LE_INDEX le_index
LE_LCM le_lcm
MAX_LE_LCM max_le_lcm
MAX_LE_LCM_EQ max_le_lcm_eq
MONOIDAL_GCD monoidal_gcd
MONOIDAL_LCM monoidal_lcm
MULTIPLES_EQ multiples_eq
MULT_GCD_LCM mult_gcd_lcm
MULT_LCM_GCD mult_lcm_gcd
NEUTRAL_GCD neutral_gcd
NEUTRAL_LCM neutral_lcm
ODD_PRIME odd_prime
PRIME prime
PRIMEPOW_DIVIDES_FACT primepow_divides_fact
PRIMEPOW_DIVIDES_INDEX primepow_divides_index
PRIMEPOW_DIVIDES_ITERATE_LCM primepow_divides_iterate_lcm
PRIMEPOW_DIVIDES_ITERATE_LCM_GEN primepow_divides_iterate_lcm_gen
PRIMEPOW_DIVIDES_LCM primepow_divides_lcm
PRIMEPOW_DIVIDES_PROD primepow_divides_prod
PRIMEPOW_DIVISORS_DIVIDES primepow_divisors_divides
PRIMEPOW_DIVISORS_EQ primepow_divisors_eq
PRIMEPOW_FACTOR primepow_factor
PRIMES_INFINITE primes_infinite
PRIME_0 prime_0
PRIME_1 prime_1
PRIME_2 prime_2
PRIME_ALT prime_alt
PRIME_COPRIME prime_coprime
PRIME_COPRIME_CASES prime_coprime_cases
PRIME_COPRIME_EQ prime_coprime_eq
PRIME_COPRIME_LT prime_coprime_lt
PRIME_COPRIME_STRONG prime_coprime_strong
PRIME_DIVEXP prime_divexp
PRIME_DIVEXP_EQ prime_divexp_eq
PRIME_DIVEXP_N prime_divexp_n
PRIME_DIVIDES_ITERATE_LCM prime_divides_iterate_lcm
PRIME_DIVIDES_ITERATE_LCM_GEN prime_divides_iterate_lcm_gen
PRIME_DIVIDES_LCM prime_divides_lcm
PRIME_DIVPROD prime_divprod
PRIME_DIVPROD_EQ prime_divprod_eq
PRIME_DIVPROD_POW prime_divprod_pow
PRIME_DIVPROD_POW_EQ prime_divprod_pow_eq
PRIME_DIVPROD_POW_GEN prime_divprod_pow_gen
PRIME_DIVPROD_POW_GEN_EQ prime_divprod_pow_gen_eq
PRIME_EXP prime_exp
PRIME_FACTOR prime_factor
PRIME_FACTORIZATION prime_factorization
PRIME_FACTORIZATION_ALT prime_factorization_alt
PRIME_FACTORIZATION_INDEX prime_factorization_index
PRIME_FACTOR_INDUCT prime_factor_induct
PRIME_FACTOR_LT prime_factor_lt
PRIME_FACTOR_PARTITION prime_factor_partition
PRIME_GE_2 prime_ge_2
PRIME_IMP_NZ prime_imp_nz
PRIME_INT_DIVPROD_EQ prime_int_divprod_eq
PRIME_IRREDUCIBLE prime_irreducible
PRIME_ODD prime_odd
PRIME_POWER_EXISTS prime_power_exists
PRIME_POWER_EXISTS_ALT prime_power_exists_alt
PRIME_POWER_EXP prime_power_exp
PRIME_POWER_MULT prime_power_mult
PRIME_PRIME_FACTOR prime_prime_factor
index_def index_def
lcm lcm
