Logipedia-Jumb

nat.lt_O_n_elim

relations.monotonic

cong.congruent_to_divides

nat.not_le_to_not_le_S_S

nat.le_to_lt_to_lt

leibniz.refl_leibniz

logic.eq_rect_r

nat.not_eq_to_eqb_false

bool.true_or_false

bool.eq_match_bool_type_true