Skip to content

Cancellation for multiplication on `nat`.

Robbert Krebbersrequested to merge
robbert/mul_reg into master

Coq's stdlib has these lemmas for Z, but those for nat are missing. We use the naming scheme of Coq's stdlib.

Edited by Robbert Krebbers

Merge request reports