Logipedia-Jumb

div_mod.eq_times_div_minus_mod

nat.axiom_plus_body_S

nat.S

bool.match_bool_prop

nat.eqb_elim

nat.eq_leb

relations.commutative

nat.times_body

nat.not_zero

nat.minus