# Pastebin REtniINM
module Max where

data Nat : Set where
  zero : Nat
  suc : Nat → Nat

max₁ : Nat → Nat → Nat
max₁ zero m = m
max₁ n zero = n
max₁ (suc n) (suc m) = suc (max₁ n m)

max₂ : Nat → Nat → Nat
max₂ n zero = n
max₂ zero m = m
max₂ (suc n) (suc m) = suc (max₂ n m)