Logipedia-Jumb

permutation.permut_S_to_permut_transpose

nat.sym_eq_minus_body_S

nat.axiom_eqb_body_O

nat.minus_le_minus_minus_comm

nat.associative_times

primes.dividesb

bigops.sub0_to_false

bool.false

nat.sym_eq_plus

nat.lt_plus_to_minus_r