Logipedia-Jumb

nat.minus_to_plus

nat.sym_eq_times

permutation.invert_permut_f

exp.exp

nat.minus_plus_plus_l

nat.plus_body

relations.transitive

nat.eq_eqb_body_S

nat.le_n_O_elim

bigops.sub0_to_false