Logipedia
Modules
About
FAQ
Search
Search
nat.axiom_plus_body_O
nat.not_le_Sn_O
cong.congruent_to_divides
nat.minus_minus
div_mod.div_mod_spec_to_eq2
nat.plus_O_n
nat.minus_minus_comm
connectives.False
bigops.sym_eq_bigop_body_O
permutation.transpose_i_j_j