Logipedia-Jumb

nat.times_Sn_m

primes.divides_to_div_mod_spec

connectives.False

nat.distributive_times_plus

bool.true_or_false

nat.not_eq_O_S

gcd.eq_gcd_aux

exp.sym_eq_exp

cong.congruent_n_n

cong.eq_times_plus_to_congruent