Associativity of (a weird) plus

PlusAssoc.agda

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ 

infix 40 _+_
_+_ : ℕ → ℕ → ℕ
zero + zero = zero
(suc a) + zero = suc a
zero + (suc b) = suc b
(suc a) + (suc b) = suc (suc (a + b))

infix 4 _≡_
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x --reflexive property
{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

cong : ∀ {A B : Set} {x y : A} (f : A → B) → x ≡ y → f x ≡ f y 
cong f refl = refl 

2+ : ∀ (a : ℕ) → ℕ
2+ a = suc (suc a) 

a+0≡a : (a : ℕ) → a + zero ≡ a
a+0≡a zero = refl
a+0≡a (suc a) = refl

0+b≡b : (b : ℕ) → zero + b ≡ b
0+b≡b zero = refl
0+b≡b (suc x) = refl

mutual

  sa+b≡s⟨a+b⟩ : (a b : ℕ) → suc a + b ≡ suc (a + b)
  sa+b≡s⟨a+b⟩ a zero rewrite a+0≡a a = refl
  sa+b≡s⟨a+b⟩ a (suc b) rewrite a+sb≡s⟨a+b⟩ a b = refl

  a+sb≡s⟨a+b⟩ : (a b : ℕ) → a + suc b ≡ suc (a + b)
  a+sb≡s⟨a+b⟩ zero b rewrite 0+b≡b b = refl
  a+sb≡s⟨a+b⟩ (suc a) b rewrite sa+b≡s⟨a+b⟩ a b = refl

+-assoc₁ : ∀ (a b c : ℕ) → a + (b + c) ≡ (a + b) + c
+-assoc₁ a b zero rewrite a+0≡a b | a+0≡a (a + b) = refl
+-assoc₁ a b (suc c)
  rewrite a+sb≡s⟨a+b⟩ b c
        | a+sb≡s⟨a+b⟩ (a + b) c
        | a+sb≡s⟨a+b⟩ a (b + c) = cong suc (+-assoc₁ a b c)