Logipedia-Jumb

bigops.sub_hk

nat.axiom_plus_body_O

cong.divides_to_congruent

nat.plus_minus

nat.le_ind

nat.axiom_eqb_body_O

nat.times

div_mod.sym_eq_mod_aux_body_O

bigops.sym_eq_bigop_body_S

gcd.sym_eq_gcd_aux_body_O