Logipedia-Jumb

logic.sym_eq

logic.eq_ind

div_mod.let_clause_1062

connectives.True

nat.sym_eq_times_body_S

nat.monotonic_le_times_r

div_mod.match_div_mod_spec_prop

bool.andb

gcd.eq_minus_gcd_aux

nat.distributive_times_plus