Logipedia-Jumb

nat.le_plus_b

nat.injective_plus_r

nat.commutative_plus

bigops.eq_bigop_S

div_mod.div_mod_spec_to_eq2

permutation.bijn

nat.commutative_times

permutation.permut

nat.sym_eq_eqb_body_O

nat.sym_eq_filter_nat_type_S