# Generated by tools/translator: qualified upstream name -> MoonBit name.
CONG_0 cong_0
CONG_MOD_0 cong_mod_0
CONG_MOD_1 cong_mod_1
CONG_MULT_LCANCEL cong_mult_lcancel
CONG_REFL cong_refl
CONG_SUB_CASES cong_sub_cases
CONG_SYM cong_sym
CONG_TRANS cong_trans
DIFFERENCE_POS_LEMMA difference_pos_lemma
EXP_EQ_MOD_CONV exp_eq_mod_conv
FERMAT_LITTLE fermat_little
FERMAT_LITTLE_PRIME fermat_little_prime
FINITE_NUMBER_SEGMENT finite_number_segment
ITSET_MODMULT itset_modmult
ITSET_MODMULT_COPRIME itset_modmult_coprime
LUCAS lucas
LUCAS_COPRIME_LEMMA lucas_coprime_lemma
LUCAS_PRIMEFACT lucas_primefact
LUCAS_WEAK lucas_weak
PHI_0 phi_0
PHI_1 phi_1
PHI_ALT phi_alt
PHI_ANOTHER phi_another
PHI_LIMIT phi_limit
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_PRIME phi_prime
PHI_PRIME_EQ phi_prime_eq
PRIMAFACT_CONTAINS primafact_contains
PRIME prime
PRIMEFACT primefact_v1
PRIMEFACT_VARIANT primefact_variant
PRIME_CONV prime_conv
PRIME_TEST prime_test
PROVE_PRIME prove_prime
PROVE_PRIMEFACT prove_primefact
certify_prime certify_prime
check_certificate check_certificate
even_num even_num
factor factor
find_primitive_root find_primitive_root
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
phi phi
powermod powermod
prime_theorem_cache prime_theorem_cache
primefact primefact
setify_num setify_num
type:certificate Certificate
uniq_num uniq_num
