Tue, 27 Mar 2012 11:45:02 +0200 | huffman | rename lemmas {divmod_int_rel_{div,mod} -> {div,mod}_int_unique, for consistency with nat lemma names | changeset | files |
Tue, 27 Mar 2012 11:41:16 +0200 | huffman | extend definition of divmod_int_rel to handle denominator=0 case | changeset | files |
Tue, 27 Mar 2012 11:02:18 +0200 | huffman | tuned proofs | changeset | files |
Tue, 27 Mar 2012 10:34:12 +0200 | huffman | shorten a proof | changeset | files |