My proofs for the Coq proof assistant
| File | Description |
|---|---|
| sum.v | Proof that 1 + 2 + ... + n = n * (n + 1) / 2 |
| sqrt_2_irrat.v | Proof that the square root of 2 is irrational |
| curry.v | Proof that for every two-parameter uncurried function, there exists an equivalent curried function |
| compose_assoc.v | Proof that function composition is associative |