Logipedia-Jumb

nat.le_to_or_lt_eq

nat.eq_eqb

nat.axiom_minus_body_O

connectives.match_And_prop

nat.le_plus_b

connectives.or_intror

div_mod.sym_eq_div_aux_body_O

nat.nat

nat.monotonic_le_plus_r

bigops.mk_ACop