A trivial proof that `x + x` is equal to `2 * x`.

Trivial.agda

module Trivial where

data Nat : Set where
    zero : Nat
    succ : Nat -> Nat
{-# BUILTIN NATURAL Nat #-}

data _==_ {A : Set} (x : A) : A -> Set where
    refl : x == x

infix 5 _==_

_+_ : Nat -> Nat -> Nat
zero + y   = y
succ x + y = succ (x + y)

infixl 6 _+_

_*_ : Nat -> Nat -> Nat
zero * y   = zero
succ x * y = (x * y) + y

infixl 7 _*_

trivial : forall (x : Nat) -> x + x == 2 * x
trivial x = refl