Logipedia-Jumb

nat.plus

permutation.permut

relations.injective

nat.sym_eq_filter_nat_type_S

fact.sym_eq_fact

primes.divides

bigops.sub0_to_false

nat.le_plus_to_minus

connectives.nmk

nat.sym_eq_eqb_body_S