Logipedia-Jumb

primes.divides_to_le

fact.eq_fact_body_O

fact.eq_fact

gcd.divides_gcd_r

cong.congruent_times

nat.le_to_not_lt

nat.eq_eqb

nat.axiom_eqb_body_O

nat.lt_O_n_elim

bigops.eq_bigop_body_S