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