Logipedia-Jumb

nat.axiom_times

nat.sym_eq_eqb

nat.lt_plus_Sn_r

logic.eq_rect_r

connectives.And

div_mod.div_mod_spec_to_eq

cong.transitive_congruent

relations.RC_reflexive

nat.lt_times

div_mod.div_aux_body