Logipedia-Jumb

nat.not_eq_to_le_to_lt

nat.filter_nat_type

bigops.bigop_false

nat.lt_to_not_eq

gcd.prime_to_gcd_1

bigops.bigop_Sfalse

nat.le_n_Sn

gcd.gcd_O_l

permutation.sym_eq_invert_permut

nat.le_plus_to_minus_r