Logipedia-Jumb

primes.divides_n_O

connectives.I

nat.le_plus

nat.eq_eqb_body_O

bigops.bigop_Strue

relations.associative

bool.match_bool_type

connectives.equal_leibniz

exp.lt_O_exp

nat.times_O_n