Logipedia
Modules
About
FAQ
Search
Search
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