Logipedia-Jumb

bigops.bigop_I_gen

connectives.Or

div_mod.axiom_mod_aux

nat.minus_S_S

nat.eq_leb

connectives.I

div_mod.eq_mod_aux_body_S

nat.transitive_le

bool.eq_match_bool_type_true

nat.monotonic_lt_times_r