Logipedia-Jumb

cong.divides_to_congruent

bigops.sub_lt

div_mod.axiom_div_aux_body_S

nat.transitive_le

relations.commutative

nat.le_to_not_lt

div_mod.div_mod_spec_to_eq2

relations.RC

nat.not_eq_to_eqb_false

logic.eq_rect_r