module pos where

open import Data.Product
open import Relation.Binary.Core
open import Data.Product1

data Nat : Set where
  zero : Nat
  suc  : (n1 : Nat) -> Nat

data Pos : ( n4 : Nat) -> Set where
  psuc : (n1 : Nat) -> Pos (suc n1)

{- splitting on first argument -}
pred0 : (n0 : Nat) -> (p : Pos n0) -> Nat 
pred0 (suc n1) p = n1
pred0 zero () 

{- splitting on second argument -}
pred1 : (n0 : Nat) -> (p : Pos n0) ->  Nat
pred1 .(suc n1) (psuc n1) = n1

{- splitting both arguments, takes two steps to check the first clause -}
pred2 : (n0 : Nat) -> (p : Pos n0) -> Nat
pred2 (suc n1) (psuc .n1) = n1 
pred2 zero ()

pred3 : (n0 : Nat) -> (p : Pos n0) -> Nat
pred3 (suc .n1) (psuc n1) = n1 
pred3 zero ()