Idris lesson: proof of plus Zero + m = m

Main.idr

module Main

data N = Zero | Succ N

add : N -> N -> N
add Zero right = right
add (Succ left) right = Succ (add left right)

plusZeroRightNat : ( right : N ) -> add Zero right = right 
plusZeroRightNat Zero = Refl

data Vector : N -> Type -> Type where
  Empty : Vector Zero t
  Cons : t -> Vector n t -> Vector (Succ n) t

concat : Vector n t -> Vector m t -> Vector (n `add` m) t
concat Empty ys = ys
concat (Cons x xs) ys = Cons x (concat xs ys)