Skip to content
GitLab

Cancellation for multiplication on `nat`.

Merged Robbert Krebbers requested 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