Logipedia-Jumb

nat.filter_nat_type

bigops.axiom_bigop_O

nat.eq_times_body_S

nat.sym_eq_filter_nat_type_O

nat.eqb

nat.eq_to_eqb_true

nat.times_body

bigops.bigop_iso

fermat.congruent_pi

nat.monotonic_le_plus_r