search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
446 stars 136 forks source link

Triangular numbers #1044

Closed felixwellen closed 7 months ago

felixwellen commented 11 months ago

Proves the usual formula for triangular numbers in this form:

(n : fst ℕ) → 2 · (∑ (first (suc n))) ≡ n · (n + 1)

Depends on #1042 #1043 (both merged now)

I just proved this, because I wondered how if it is as little work as I thought it is. Judging from this PR, it looks pleasant, but I actually had to do some refactoring to make it so.

felixwellen commented 7 months ago

Thanks! Merging when CI is happy.