Logipedia-Jumb

nat.eq_eqb_body_O

permutation.permut

nat.eqb_false_to_not_eq

gcd.prime_to_gcd_1

nat.plus_n_Sm

logic.eq_f2

bigops.sub_lt

nat.commutative_plus

nat.axiom_times_body_O

logic.eq_coerc