import
import_segment "hol4"
const_maps
"divides" > "Rings.dvd_class.dvd" :: "nat => nat => bool"
thm_maps
"divides_def" > "Compatibility.divides_def"
"ONE_DIVIDES_ALL" > "GCD.gcd_lcm_complete_lattice_nat.bot_least"
"NOT_LT_DIV" > "Nat.nat_dvd_not_less"
"DIVIDES_TRANS" > "Nat.dvd.order_trans"
"DIVIDES_SUB" > "Nat.dvd_diff_nat"
"DIVIDES_REFL" > "Nat.dvd.order_refl"
"DIVIDES_MULT_LEFT" > "HOL4Base.divides.DIVIDES_MULT_LEFT"
"DIVIDES_MULT" > "Rings.comm_semiring_1_class.dvd_mult2"
"DIVIDES_LE" > "Nat.dvd_imp_le"
"DIVIDES_FACT" > "HOL4Base.divides.DIVIDES_FACT"
"DIVIDES_ANTISYM" > "Nat.dvd.antisym"
"DIVIDES_ADD_2" > "Primes.divides_add_revr"
"DIVIDES_ADD_1" > "Rings.comm_semiring_1_class.dvd_add"
"ALL_DIVIDES_0" > "GCD.gcd_lcm_complete_lattice_nat.top_greatest"
end