# Generated by tools/translator: qualified upstream name -> MoonBit name.
ADD add
ADD1 add1
ADD_0 add_0
ADD_AC add_ac
ADD_ASSOC add_assoc
ADD_CLAUSES add_clauses
ADD_EQ_0 add_eq_0
ADD_SUB add_sub
ADD_SUB2 add_sub2
ADD_SUBR add_subr
ADD_SUBR2 add_subr2
ADD_SUC add_suc
ADD_SYM add_sym
BIT0 bit0
BIT0_THM bit0_thm
BIT1 bit1
BIT1_THM bit1_thm
BITS_ELIM_CONV bits_elim_conv
DEPENDENT_CHOICE dependent_choice
DEPENDENT_CHOICE_FIXED dependent_choice_fixed
DIVISION division
DIVISION_0 division_0
DIVISION_SIMP division_simp
DIVMOD_ELIM_THM divmod_elim_thm
DIVMOD_ELIM_THM' divmod_elim_thm_p
DIVMOD_EXIST divmod_exist
DIVMOD_EXIST_0 divmod_exist_0
DIVMOD_UNIQ divmod_uniq
DIVMOD_UNIQ_LEMMA divmod_uniq_lemma
DIV_0 div_0
DIV_1 div_1
DIV_ADD_EQ div_add_eq
DIV_ADD_EQ_EQ div_add_eq_eq
DIV_ADD_MOD div_add_mod
DIV_DIV div_div
DIV_EQ_0 div_eq_0
DIV_EQ_EXCLUSION div_eq_exclusion
DIV_EQ_SELF div_eq_self
DIV_EXP div_exp
DIV_LE div_le
DIV_LE_EXCLUSION div_le_exclusion
DIV_LT div_lt
DIV_MOD div_mod
DIV_MONO div_mono
DIV_MONO2 div_mono2
DIV_MONO_LT div_mono_lt
DIV_MULT div_mult
DIV_MULT2 div_mult2
DIV_MULT_ADD div_mult_add
DIV_MUL_LE div_mul_le
DIV_REFL div_refl
DIV_UNIQ div_uniq
DIV_ZERO div_zero
DOUBLE_HALF double_half
EQ_ADD_LCANCEL eq_add_lcancel
EQ_ADD_LCANCEL_0 eq_add_lcancel_0
EQ_ADD_RCANCEL eq_add_rcancel
EQ_ADD_RCANCEL_0 eq_add_rcancel_0
EQ_DIVMOD eq_divmod
EQ_EXP eq_exp
EQ_IMP_LE eq_imp_le
EQ_MULT_LCANCEL eq_mult_lcancel
EQ_MULT_RCANCEL eq_mult_rcancel
EVEN even
EVEN_ADD even_add
EVEN_AND_ODD even_and_odd
EVEN_DOUBLE even_double
EVEN_EXISTS even_exists
EVEN_EXISTS_LEMMA even_exists_lemma
EVEN_EXP even_exp
EVEN_MOD even_mod
EVEN_MOD_EVEN even_mod_even
EVEN_MULT even_mult
EVEN_ODD_DECOMPOSITION even_odd_decomposition
EVEN_OR_ODD even_or_odd
EVEN_SUB even_sub
EXISTS_LT_MOD_THM exists_lt_mod_thm
EXISTS_MOD_THM exists_mod_thm
EXP exp
EXP_1 exp_1
EXP_2 exp_2
EXP_ADD exp_add
EXP_EQ_0 exp_eq_0
EXP_EQ_1 exp_eq_1
EXP_EXP exp_exp
EXP_LT_0 exp_lt_0
EXP_MONO_EQ exp_mono_eq
EXP_MONO_LE exp_mono_le
EXP_MONO_LE_IMP exp_mono_le_imp
EXP_MONO_LT exp_mono_lt
EXP_MONO_LT_IMP exp_mono_lt_imp
EXP_MULT exp_mult
EXP_ONE exp_one
EXP_ZERO exp_zero
FACT fact
FACT_LE fact_le
FACT_LT fact_lt
FACT_MONO fact_mono
FACT_NZ fact_nz
FORALL_LT_MOD_THM forall_lt_mod_thm
FORALL_MOD_THM forall_mod_thm
GE ge
GT gt
HALF_DOUBLE half_double
LDIV_LT_EQ ldiv_lt_eq
LE le
LEFT_ADD_DISTRIB left_add_distrib
LEFT_SUB_DISTRIB left_sub_distrib
LET_ADD2 let_add2
LET_ANTISYM let_antisym
LET_CASES let_cases
LET_TRANS let_trans
LE_0 le_0
LE_1 le_1
LE_ADD le_add
LE_ADD2 le_add2
LE_ADDR le_addr
LE_ADD_LCANCEL le_add_lcancel
LE_ADD_RCANCEL le_add_rcancel
LE_ANTISYM le_antisym
LE_CASES le_cases
LE_EXISTS le_exists
LE_EXP le_exp
LE_IMP le_imp
LE_INDUCT le_induct
LE_LDIV le_ldiv
LE_LDIV_EQ le_ldiv_eq
LE_LT le_lt
LE_MINIMAL le_minimal
LE_MULT2 le_mult2
LE_MULT_LCANCEL le_mult_lcancel
LE_MULT_RCANCEL le_mult_rcancel
LE_RDIV_EQ le_rdiv_eq
LE_REFL le_refl
LE_SQUARE_REFL le_square_refl
LE_SUC le_suc
LE_SUC_LT le_suc_lt
LE_TRANS le_trans
LT lt
LTE_ADD2 lte_add2
LTE_ANTISYM lte_antisym
LTE_CASES lte_cases
LTE_TRANS lte_trans
LT_0 lt_0
LT_ADD lt_add
LT_ADD2 lt_add2
LT_ADDR lt_addr
LT_ADD_LCANCEL lt_add_lcancel
LT_ADD_RCANCEL lt_add_rcancel
LT_ANTISYM lt_antisym
LT_CASES lt_cases
LT_EXISTS lt_exists
LT_EXP lt_exp
LT_IMP_LE lt_imp_le
LT_IMP_NE lt_imp_ne
LT_LE lt_le
LT_LMULT lt_lmult
LT_MULT lt_mult
LT_MULT2 lt_mult2
LT_MULT_LCANCEL lt_mult_lcancel
LT_MULT_RCANCEL lt_mult_rcancel
LT_NZ lt_nz
LT_POW2_REFL lt_pow2_refl
LT_REFL lt_refl
LT_SUC lt_suc
LT_SUC_LE lt_suc_le
LT_TRANS lt_trans
MAX max
MIN min
MINIMAL minimal_v1
MINIMAL_LBOUND minimal_lbound
MINIMAL_LE minimal_le
MINIMAL_MONO minimal_mono
MINIMAL_UBOUND minimal_ubound
MINIMAL_UNIQUE minimal_unique
MOD_0 mod_0
MOD_1 mod_1
MOD_2_CASES mod_2_cases
MOD_ADD_CASES mod_add_cases
MOD_ADD_EQ mod_add_eq
MOD_ADD_EQ_EQ mod_add_eq_eq
MOD_ADD_MOD mod_add_mod
MOD_CASES mod_cases
MOD_DIV_EQ_0 mod_div_eq_0
MOD_DOWN_CONV mod_down_conv
MOD_EQ mod_eq
MOD_EQ_0 mod_eq_0
MOD_EQ_SELF mod_eq_self
MOD_EVEN_2 mod_even_2
MOD_EXISTS mod_exists
MOD_EXP mod_exp
MOD_EXP_MOD mod_exp_mod
MOD_LE mod_le
MOD_LE_TWICE mod_le_twice
MOD_LT mod_lt
MOD_LT_EQ mod_lt_eq
MOD_LT_EQ_LT mod_lt_eq_lt
MOD_MOD mod_mod
MOD_MOD_EXP_MIN mod_mod_exp_min
MOD_MOD_LE mod_mod_le
MOD_MOD_REFL mod_mod_refl
MOD_MULT mod_mult
MOD_MULT2 mod_mult2
MOD_MULT_ADD mod_mult_add
MOD_MULT_LMOD mod_mult_lmod
MOD_MULT_MOD mod_mult_mod
MOD_MULT_MOD2 mod_mult_mod2
MOD_MULT_RMOD mod_mult_rmod
MOD_REFL mod_refl
MOD_UNIQ mod_uniq
MOD_ZERO mod_zero
MULT mult
MULT_0 mult_0
MULT_2 mult_2
MULT_AC mult_ac
MULT_ASSOC mult_assoc
MULT_CLAUSES mult_clauses
MULT_DIV_LE mult_div_le
MULT_EQ_0 mult_eq_0
MULT_EQ_1 mult_eq_1
MULT_EXP mult_exp
MULT_SUC mult_suc
MULT_SYM mult_sym
NOT_EVEN not_even
NOT_LE not_le
NOT_LT not_lt
NOT_ODD not_odd
NUM_CANCEL_CONV num_cancel_conv
ODD odd
ODD_ADD odd_add
ODD_DOUBLE odd_double
ODD_EXISTS odd_exists
ODD_EXP odd_exp
ODD_MOD odd_mod
ODD_MOD_EVEN odd_mod_even
ODD_MULT odd_mult
ODD_SUB odd_sub
ONE one
PRE pre
PRE_ELIM_THM pre_elim_thm
PRE_ELIM_THM' pre_elim_thm_p
RDIV_LT_EQ rdiv_lt_eq
RIGHT_ADD_DISTRIB right_add_distrib
RIGHT_SUB_DISTRIB right_sub_distrib
SUB sub
SUB_0 sub_0
SUB_ADD sub_add
SUB_ADD_LCANCEL sub_add_lcancel
SUB_ADD_RCANCEL sub_add_rcancel
SUB_ELIM_THM sub_elim_thm
SUB_ELIM_THM' sub_elim_thm_p
SUB_EQ_0 sub_eq_0
SUB_PRESUC sub_presuc
SUB_REFL sub_refl
SUB_SUC sub_suc
SUC_SUB1 suc_sub1
TRANSITIVE_STEPWISE_LE transitive_stepwise_le
TRANSITIVE_STEPWISE_LE_EQ transitive_stepwise_le_eq
TRANSITIVE_STEPWISE_LT transitive_stepwise_lt
TRANSITIVE_STEPWISE_LT_EQ transitive_stepwise_lt_eq
TWO two
WLOG_LE wlog_le
WLOG_LE_3 wlog_le_3
WLOG_LT wlog_lt
minimal minimal
num_INDUCTION_DOWN num_induction_down
num_MAX num_max
num_WF num_wf
num_WOP num_wop
