Logipedia-Jumb

connectives.or_introl

div_mod.sym_eq_div_aux_body_O

div_mod.mod_O_n

nat.le_to_not_lt

nat.le

relations.injective

permutation.transpose_transpose

div_mod.eq_div_O

nat.axiom_match_nat_type_O

cong.congruent