create_nat set_to_zero_nat blit_nat set_digit_nat nth_digit_nat num_digits_nat num_leading_zero_bits_in_digit is_digit_int is_digit_zero is_digit_normalized is_digit_odd incr_nat add_nat complement_nat decr_nat sub_nat mult_digit_nat mult_nat shift_left_nat div_digit_nat div_nat shift_right_nat compare_digits_nat compare_nat land_digit_nat lor_digit_nat lxor_digit_nat