Logipedia
Modules
About
FAQ
Search
Search
nat.eq_filter_nat_type_S
nat.minus_n_O
nat.le_pred_n
bigops.sub0_to_false
nat.le
div_mod.eq_div_aux_body_S
nat.not_le_to_not_le_S_S
div_mod.div_mod_spec_to_eq
cong.transitive_congruent
primes.dividesb_true_to_divides