open import Relation.Binary.PropositionalEquality
open import nat
open import nat_add

module three_plus_one where

3+1 : (S (S (S O)))  +  (S O) !$\equiv$! (S (S (S (S O))))
3+1 = refl