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

Merge request reports