Logipedia-Jumb

connectives.or_intror

fact.sym_eq_fact_body_O

div_mod.le_mod_aux_m_m

nat.leb_body

div_mod.div_times

nat.eq_minus_body_O

nat.times_O_n

bigops.bigop_body

nat.times_body

nat.eq_eqb