# Generated by tools/translator: qualified upstream name -> MoonBit name.
CHINESE_REMAINDER_COPRIME_COUNT chinese_remainder_coprime_count
CHINESE_REMAINDER_COPRIME_UNIQUE chinese_remainder_coprime_unique
CHINESE_REMAINDER_COUNT chinese_remainder_count
CHINESE_REMAINDER_UNIQUE chinese_remainder_unique
CHINESE_REMAINDER_USUAL chinese_remainder_usual
CONG_0 cong_0
CONG_0_DIVIDES cong_0_divides
CONG_1_DIVIDES cong_1_divides
CONG_1_DIVIDES_EQ cong_1_divides_eq
CONG_ADD cong_add
CONG_ADD_LCANCEL cong_add_lcancel
CONG_ADD_LCANCEL_EQ cong_add_lcancel_eq
CONG_ADD_LCANCEL_EQ_0 cong_add_lcancel_eq_0
CONG_ADD_RCANCEL cong_add_rcancel
CONG_ADD_RCANCEL_EQ cong_add_rcancel_eq
CONG_ADD_RCANCEL_EQ_0 cong_add_rcancel_eq_0
CONG_CASE cong_case
CONG_CASES cong_cases
CONG_CHINESE cong_chinese
CONG_CHINESE_EQ cong_chinese_eq
CONG_CONV cong_conv
CONG_COPRIME cong_coprime
CONG_DIV cong_div
CONG_DIVIDES cong_divides
CONG_DIVIDES_MODULUS cong_divides_modulus
CONG_DIV_COPRIME cong_div_coprime
CONG_EXP cong_exp
CONG_EXP_1 cong_exp_1
CONG_GCD_LEFT cong_gcd_left
CONG_GCD_RIGHT cong_gcd_right
CONG_IMP_EQ cong_imp_eq
CONG_LE cong_le
CONG_LMUL cong_lmul
CONG_LT cong_lt
CONG_MINUS1 cong_minus1
CONG_MINUS1_SQUARED cong_minus1_squared
CONG_MOD cong_mod
CONG_MOD_0 cong_mod_0
CONG_MOD_1 cong_mod_1
CONG_MOD_2 cong_mod_2
CONG_MOD_2_ALT cong_mod_2_alt
CONG_MOD_LT cong_mod_lt
CONG_MOD_SQUAREFREE cong_mod_squarefree
CONG_MOD_SQUAREFREE_EQ cong_mod_squarefree_eq
CONG_MULT cong_mult
CONG_MULT_1 cong_mult_1
CONG_MULT_LCANCEL cong_mult_lcancel
CONG_MULT_LCANCEL_ALL cong_mult_lcancel_all
CONG_MULT_LCANCEL_EQ cong_mult_lcancel_eq
CONG_MULT_RCANCEL cong_mult_rcancel
CONG_MULT_RCANCEL_EQ cong_mult_rcancel_eq
CONG_REFL cong_refl
CONG_RMUL cong_rmul
CONG_SOLVE cong_solve
CONG_SOLVE_EQ cong_solve_eq
CONG_SOLVE_LT_EQ cong_solve_lt_eq
CONG_SOLVE_UNIQUE cong_solve_unique
CONG_SOLVE_UNIQUE_NONTRIVIAL cong_solve_unique_nontrivial
CONG_SQUARE_1_PRIME_POWER cong_square_1_prime_power
CONG_SUB cong_sub
CONG_SUB_CASES cong_sub_cases
CONG_SYM cong_sym
CONG_TO_1 cong_to_1
CONG_TRANS cong_trans
CONG_UNIQUE_INVERSE_PRIME cong_unique_inverse_prime
COPRIME_ORDER coprime_order
COUNT_CONG_SOLVE count_cong_solve
COUNT_CONG_SOLVE_GEN count_cong_solve_gen
COUNT_CONG_SOLVE_SIMPLE count_cong_solve_simple
COUNT_ROOTS_MODULO_COPRIME count_roots_modulo_coprime
EQ_IMP_CONG eq_imp_cong
EVEN_MOD_2 even_mod_2
EVEN_PHI even_phi
EVEN_PHI_EQ even_phi_eq
EXP_ITER exp_iter
FERMAT_LITTLE fermat_little
FERMAT_LITTLE_PRIME fermat_little_prime
FINITE_NUMBER_SEGMENT finite_number_segment
GUIDED_PROVE_PRIME guided_prove_prime
INJECTIVE_EXP_MODULO injective_exp_modulo
INVERSE_MOD_1 inverse_mod_1
INVERSE_MOD_BOUND inverse_mod_bound
INVERSE_MOD_BOUND_LE inverse_mod_bound_le
INVERSE_MOD_CONG inverse_mod_cong
INVERSE_MOD_CONV inverse_mod_conv
INVERSE_MOD_INVERSE_MOD inverse_mod_inverse_mod
INVERSE_MOD_INVERSE_MOD_CONG inverse_mod_inverse_mod_cong
INVERSE_MOD_INVERSION inverse_mod_inversion
INVERSE_MOD_LMUL inverse_mod_lmul
INVERSE_MOD_LMUL_EQ inverse_mod_lmul_eq
INVERSE_MOD_LMUL_GEN inverse_mod_lmul_gen
INVERSE_MOD_NONZERO inverse_mod_nonzero
INVERSE_MOD_NONZERO_ALT inverse_mod_nonzero_alt
INVERSE_MOD_RMUL inverse_mod_rmul
INVERSE_MOD_RMUL_EQ inverse_mod_rmul_eq
INVERSE_MOD_RMUL_GEN inverse_mod_rmul_gen
INVERSE_MOD_UNIQUE inverse_mod_unique
ITERATE_ITERATE_DIVISORS iterate_iterate_divisors
ITERATE_OVER_COPRIME iterate_over_coprime
LUCAS lucas
LUCAS_COPRIME_LEMMA lucas_coprime_lemma
LUCAS_PRIMEFACT lucas_primefact
LUCAS_WEAK lucas_weak
MOD_MULT_CONG mod_mult_cong
MOD_UNIQUE mod_unique
NPRODUCT_CMUL nproduct_cmul
NPRODUCT_MOD nproduct_mod
ODD_MOD_2 odd_mod_2
ODD_PHI_EQ odd_phi_eq
ORDER order_v1
ORDER_1 order_1
ORDER_CONG order_cong
ORDER_DIVIDES order_divides
ORDER_DIVIDES_EXPDIFF order_divides_expdiff
ORDER_DIVIDES_MAXIMAL order_divides_maximal
ORDER_DIVIDES_PHI order_divides_phi
ORDER_EQ_0 order_eq_0
ORDER_EQ_1 order_eq_1
ORDER_EXP order_exp
ORDER_EXP_GEN order_exp_gen
ORDER_INVERSE_MOD order_inverse_mod
ORDER_LCM_EXISTS order_lcm_exists
ORDER_LE_PHI order_le_phi
ORDER_MINIMAL order_minimal
ORDER_MOD order_mod
ORDER_MUL_DIVIDES order_mul_divides
ORDER_MUL_EQ order_mul_eq
ORDER_MUL_LCM order_mul_lcm
ORDER_UNIQUE order_unique
ORDER_UNIQUE_ALT order_unique_alt
ORDER_UNIQUE_PRIME order_unique_prime
ORDER_WORKS order_works
PARI_THRESHOLD pari_threshold
PHI_0 phi_0
PHI_1 phi_1
PHI_2 phi_2
PHI_ALT phi_alt
PHI_ANOTHER phi_another
PHI_EQ_0 phi_eq_0
PHI_EQ_PRIME phi_eq_prime
PHI_FINITE_LEMMA phi_finite_lemma
PHI_LIMIT phi_limit
PHI_LIMIT_COMPOSITE phi_limit_composite
PHI_LIMIT_STRONG phi_limit_strong
PHI_LOWERBOUND_1 phi_lowerbound_1
PHI_LOWERBOUND_1_STRONG phi_lowerbound_1_strong
PHI_LOWERBOUND_2 phi_lowerbound_2
PHI_MULTIPLICATIVE phi_multiplicative
PHI_PRIME phi_prime
PHI_PRIMEPOW phi_primepow
PHI_PRIMEPOW_ALT phi_primepow_alt
PHI_PRIMEPOW_SUC phi_primepow_suc
PHI_PRIME_EQ phi_prime_eq
POCKLINGTON pocklington
POCKLINGTON_ALT pocklington_alt
POCKLINGTON_LEMMA pocklington_lemma
POCKLINGTON_PRIMEFACT pocklington_primefact
POWER_RESIDUE_MODULO_COPRIME power_residue_modulo_coprime
POWER_RESIDUE_MODULO_PRIME power_residue_modulo_prime
PRIMAFACT_CONTAINS primafact_contains
PRIMEFACT primefact_v1
PRIMEFACT_VARIANT primefact_variant
PRIME_CONV prime_conv
PRIME_DIVISOR_SQRT prime_divisor_sqrt
PRIME_IMP_SQUAREFREE prime_imp_squarefree
PRIME_PRIME_FACTOR_SQRT prime_prime_factor_sqrt
PRIME_RULE prime_rule
PRIME_TEST prime_test
PRIMITIVE_ROOT_IMAGE primitive_root_image
PRIMITIVE_ROOT_IMAGE_PRIME primitive_root_image_prime
PRIMITIVE_ROOT_IMP_COPRIME primitive_root_imp_coprime
PRIMITIVE_ROOT_IMP_PRIME primitive_root_imp_prime
PRIMITIVE_ROOT_SURJECTIVE primitive_root_surjective
PRIMITIVE_ROOT_SURJECTIVE_ALT primitive_root_surjective_alt
PRIMITIVE_ROOT_SURJECTIVE_PRIME primitive_root_surjective_prime
PRIMITIVE_ROOT_SURJECTIVE_PRIME_ALT primitive_root_surjective_prime_alt
PROVE_PRIME prove_prime
PROVE_PRIMEFACT prove_primefact
SQUAREFREE squarefree_v1
SQUAREFREE_0 squarefree_0
SQUAREFREE_1 squarefree_1
SQUAREFREE_ALT squarefree_alt
SQUAREFREE_COPRIME squarefree_coprime
SQUAREFREE_COPRIME_DIVISORS squarefree_coprime_divisors
SQUAREFREE_DECOMPOSITION squarefree_decomposition
SQUAREFREE_DIVEXP squarefree_divexp
SQUAREFREE_DIVEXP_EQ squarefree_divexp_eq
SQUAREFREE_DIVIDES squarefree_divides
SQUAREFREE_DIVISOR squarefree_divisor
SQUAREFREE_EXP squarefree_exp
SQUAREFREE_EXPAND squarefree_expand
SQUAREFREE_EXPAND_EQ squarefree_expand_eq
SQUAREFREE_GCD squarefree_gcd
SQUAREFREE_GCD_SQUARE squarefree_gcd_square
SQUAREFREE_IMP_NZ squarefree_imp_nz
SQUAREFREE_INDEX squarefree_index
SQUAREFREE_MUL squarefree_mul
SQUAREFREE_NPRODUCT squarefree_nproduct
SQUAREFREE_PRIME squarefree_prime
SQUAREFREE_PRIME_DIVISOR squarefree_prime_divisor
SQUAREFREE_PRIME_INDEX squarefree_prime_index
certify_prime certify_prime
check_certificate check_certificate
even_num even_num
extract_primes_from_certificate extract_primes_from_certificate
factor factor
find_primitive_root find_primitive_root
general_certify_prime general_certify_prime
guided_certify_prime guided_certify_prime
inverse_mod inverse_mod
log2 log2
lookup_under_num lookup_under_num
multifactor multifactor
nat_mod nat_mod
nat_mod_lemma nat_mod_lemma
num_0 num_0
num_1 num_1
num_2 num_2
odd_num odd_num
order order
phi phi
powermod powermod
prime_theorem_cache prime_theorem_cache
primefact primefact
setify_num setify_num
split_factors split_factors
squarefree squarefree
type:certificate Certificate
uniq_num uniq_num
