Logipedia-Jumb

nat.distributive_times_plus

nat.not_lt_to_le

div_mod.sym_eq_mod_aux

cong.let_clause_73

logic.rewrite_l

connectives.I

nat.lt_O_S

permutation.eq_to_bijn

leibniz.sym_leibniz

logic.eq_ind_r