Logipedia-Jumb

div_mod.mod_O_n

nat.minus_n_O

div_mod.div_mod_spec

bigops.sym_eq_bigop_body_O

nat.le_plus_to_le

relations.transitive

nat.lt_O_S

gcd.eq_minus_gcd

nat.axiom_plus_body_O

nat.pred_Sn