Associativity of addition

{-# OPTIONS --without-K --safe #-}

module simplethms-2 where

Ιnstead of copying definition, let us just import them from Propositional Equality. This way we are going to have access to the names defined there:

import simplethms-1

This makes it visible, but we don not want to write things like: simplethms-1._≡_, so we open it:

open simplethms-1

A convenient shorthand is

open import <module>

in one line.

Addition is associative

We want to prove the following statement:

is-assoc+ : (x y z : ℕ) → x + (y + z) ≡ (x + y) + z

To prove it, we use the same techniques as before with rewrite after case splitting on the constructor in the first variable:

is-assoc+ zero y z = refl
is-assoc+ (suc x) y z rewrite is-assoc+ x y z = refl