module nat where

open import Data.Nat using (ℕ; zero; suc; _+_)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; step-≡-∣; step-≡-⟩; _∎)


+-right-suc : Set
+-right-suc = ∀ (x y : ℕ) → x + suc y ≡ suc (x + y)

+-right-suc-proof : ∀ (x y : ℕ) → x + suc y ≡ suc (x + y)
+-right-suc-proof zero y =
  begin
    zero + suc y
    ≡⟨⟩
    suc y
    ≡⟨⟩
    suc (zero + y)
   ∎
+-right-suc-proof (suc x) y =
  begin
    (suc x) + (suc y)
  ≡⟨⟩
    suc(x + (suc y))
  ≡⟨ cong suc (+-right-suc-proof x y) ⟩
    suc(suc(x + y))
  ∎

+-comm : Set
+-comm = ∀ (x y : ℕ) → x + y  ≡ y + x

+-comm-proof : ∀ (x y : ℕ) → x + y  ≡ y + x
+-comm-proof zero zero = refl
+-comm-proof zero (suc y) = 
  begin
    zero + (suc y)
  ≡⟨⟩
    suc y
  ≡⟨ cong suc (+-comm-proof zero y) ⟩
    suc (y + zero)
  ≡⟨⟩
    (suc y) + zero
  ∎
+-comm-proof (suc x) zero =
  begin
    (suc x) + zero
  ≡⟨⟩
    suc (x + zero)
  ≡⟨ cong suc (+-comm-proof x zero) ⟩
    suc (zero + x)
  ≡⟨⟩
    suc x
  ≡⟨⟩
    zero + (suc x)
  ∎
+-comm-proof (suc x) (suc y) rewrite +-right-suc-proof x y | +-comm-proof x y | +-right-suc-proof y x = refl