Logipedia-Jumb

div_mod.sym_eq_mod_aux_body_O

nat.distributive_times_plus_r

fact.eq_fact_body_S

div_mod.axiom_div_aux

nat.axiom_times_body_S

bigops.eq_bigop_S

nat.associative_plus

relations.commutative

nat.le_n

exp.sym_eq_exp