Logipedia-Jumb

nat.minus_le_minus_minus_comm

div_mod.div_mod_spec_intro

bool.bool

permutation.axiom_invert_permut_body_O

fermat.congruent_exp_pred_SO

nat.le_n

div_mod.eq_div_aux

nat.le_gen

cong.congruent_times

bigops.eq_bigop_S