Logipedia-Jumb

nat.le_plus_b

bigops.eq_bigop_body_S

connectives.match_Or_prop

fermat.prime_to_not_divides_fact

nat.monotonic_lt_times_r

bigops.bigop_I_gen

div_mod.lt_mod_m_m

cong.mod_times

nat.monotonic_le_minus_r

nat.eq_leb_body_O