Logipedia-Jumb

primes.divides_to_le

fact.eq_fact

gcd.divides_gcd_nm

exp.sym_eq_exp_body_O

logic.sym_not_eq

nat.le_S_S_to_le

nat.monotonic_le_plus_l

relations.injective

div_mod.axiom_mod_aux_body_S

nat.injective_plus_r