Logipedia-Jumb

nat.eq_minus

fact.axiom_fact_body_S

nat.eq_leb_body_O

primes.divides_to_div_mod_spec

cong.let_clause_73

div_mod.eq_div_aux

connectives.I

nat.minus

nat.decidable_lt

gcd.prime_to_gcd_1