Logipedia-Jumb

relations.distributive

logic.decidable

div_mod.sym_eq_div_aux_body_S

nat.S_pred

primes.divides_to_div_mod_spec

logic.trans_eq

nat.le_n

nat.distributive_times_plus

nat.lt_S_to_lt

nat.le_plus