Logipedia-Jumb

permutation.permut_to_bijn

primes.divides_n_O

permutation.eq_to_bijn

nat.sym_eq_times_body_S

nat.le_S_S

nat.le_to_not_lt

nat.distributive_times_minus

primes.prime_to_lt_SO

nat.eq_plus_body_S

nat.associative_times