Logipedia-Jumb

nat.eqb_n_n

connectives.Or

nat.le_S_S_to_le

nat.eq_plus

nat.lt_to_le_to_lt_times

exp.sym_eq_exp_body_S

div_mod.sym_eq_mod_aux

exp.exp

logic.eq_ind_r

div_mod.div_aux