search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.23k stars 185 forks source link

injectivity of nat addition #1973

Closed Alizter closed 1 month ago

Alizter commented 1 month ago

This is a simple lemma that comes in useful later. We could probably give a shorter proof with commutativity of nat addition, but I would prefer to keep this earlier on.

Alizter commented 1 month ago

I can't remember my reasoning now so it probably wasn't very good. I think I may have confused myself about where the commutativity lemma was and perhaps thought it was in Arithmetic. I've updated the proof to use commutativity now.