Logipedia-Jumb

nat.not_le_S_S_to_not_le

nat.axiom_leb_body_O

nat.monotonic_lt_plus_r

nat.axiom_filter_nat_type_O

leibniz.sym_leibniz

nat.nat_ind

connectives.conj

exp.axiom_exp_body_S

primes.divides_to_mod_O

primes.match_divides_prop