Logipedia-Jumb

nat.eq_filter_nat_type_S

nat.minus_n_O

nat.le_pred_n

bigops.sub0_to_false

nat.le

div_mod.eq_div_aux_body_S

nat.not_le_to_not_le_S_S

div_mod.div_mod_spec_to_eq

cong.transitive_congruent

primes.dividesb_true_to_divides