Logipedia-Jumb

nat.le_plus_n

relations.associative

permutation.injective_invert_permut

nat.eq_eqb_body_S

nat.sym_eq_minus

nat.minus_n_O

logic.trans_eq

gcd.let_clause_15491

nat.monotonic_le_plus_r

div_mod.lt_mod_m_m