Logipedia-Jumb

gcd.eq_gcd_aux_body_S

nat.axiom_times_body_S

nat.lt_to_le_to_lt_times

nat.le_plus_b

exp.axiom_exp_body_S

fact.axiom_fact_body_O

nat.distributive_times_plus_r

nat.plus_n_Sm

div_mod.div_mod

bigops.eq_bigop_body_O