Skip to content

Cancellation for multiplication on `nat`.

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