Logipedia-Jumb

cong.mod_mod

nat.monotonic_pred

nat.axiom_eqb

nat.pred

nat.eq_minus_body_O

nat.sym_eq_leb_body_S

nat.minus_n_n

permutation.bijn_n_Sn

div_mod.eq_times_div_minus_mod

nat.minus_S_S