Logipedia-Jumb

nat.le_to_not_lt

connectives.False

nat.le_plus_b

permutation.eq_invert_permut_body_S

primes.quotient

nat.eq_match_nat_type_S

nat.sym_eq_leb_body_S

nat.axiom_times

connectives.True

nat.lt_times